Алексей Махоткин

домашняя страница

Критика Standard ML — полное формальное определение

Andrew W. Appel, «Критика Standard ML», оглавление

Язык программирования Pascal был шагом вперед в разработке языков программирования, и он стал чрезвычайно популярен по нескольким причинам. Он поддерживал ясные и полезные управляющие конструкции и структуры данных. Это достаточно небольшой язык, и он был достаточно точно описан в спецификации (неформально написанной), поэтому люди хорошо понимали, что делает та или иная программа на Pascal.

Однако, в Pascal до сих пор есть «двусмысленности и небезопасные места». То бишь, определение языка неоднозначно определяет некоторые конструкции (и различные компиляторы дают различные результаты для одной и той же программы); сам язык небезопасен: он не «безопасен» в смысле, описанном Хоаром.

ML не только безопасен, но и однозначно определен. «Определение Standard ML» содержит полную операциональную семантику всего языка. Можно использовать «Определение» для точного вычисления, какие программы будут приняты компилятором, и каковы будут их результаты.

Более того, «Определение» (с сопутствующими комментариями) полностью читабельно — насколько вообще читабельны формальные определения семантики. Это не означает, что определение можно использовать в качестве руководства для программиста: в нем слишком много формальной нотации и слишком мало рабочих примеров. Однако изучающие разработку языков программирования, или же серьезные писатели компиляторов, могут использовать «Определение» в качестве справочного руководства, чтобы в случае сомнений понять значение каждой конструкции. Это приводит к переносимости между реализациями, к принципиальной возможности доказать корректность программы, и к уверенности в безопасности программы на ML.

С течением времени «Определение» доказало свою пригодность в качестве основы для полезных технических дискуссий между читателями. Даже когда в «Определении» обнаруживались непроработанные места, их можно было обсуждать и с уверенностью исправлять, при этом достигалось полное согласие относительно того, что именно означают изменения.

Формальное определение может быть лишь сложным талисманом, если его не получается использовать для доказательства важных возможностей языка. «Определение» хорошо пригодно для математического доказательства, что, например, программы, проверяющие тип, будут исполняться «безопасно», и что не появятся «висячие ссылки» (неверные указатели), и что алгоритм выведения типов всегда обнаруживает самый общий тип для выражения, и множество других теорем, которые внушают уверенность в семантике языка (Некоторые из перечисленных теорем, на самом деле, были доказаны только для подмножеств Standard ML.).

Сторонники формального описания языков программирования издавна заявляли, что семантику следует использовать в качестве инструмента разработки языка программирования, а не просто инструмента записи семантики существующего языка. Краткость и полнота «Определения ML» являются следствием, в частности, того, что комитет по разработке Standard ML сопротивляется внесению в язык возможностей, для которых непонятно, как записать семантику с доказанной корректностью.

Comments