Семья лиственницы

Семейство Larch языков формальных спецификаций предназначено для точной спецификации вычислительных систем. Они позволяют четко определять компьютерные программы и формулировать доказательства поведения программ. ^[1]

Семейство Larch было разработано в основном в США в 1980-х и 1990-х годах с участием исследователей из Xerox PARC , Центра системных исследований DEC (DEC/SRC), Массачусетского технологического института (MIT) и других мест. В отличие от нотации Z , семейство Larch имеет один язык для алгебраической спецификации абстрактных типов данных ( Larch Shared Language (LSL)), а также отдельный язык интерфейса, адаптированный для каждого языка, на котором должны быть написаны программы, например C , Modula. -3 , Smalltalk и т. д. В рамках проекта Larch также были разработаны инструменты для поддержки использования формальных спецификаций, включая Larch Prover (LP).

См. также

Формальные методы

Ссылки

^ Гуттаг, Джон В.; Хорнинг, Джеймс Дж. (1993). Larch: Языки и инструменты для формальной спецификации (PDF) . Спрингер-Верлаг . ISBN 978-1-4612-2704-5 .

Внешние ссылки

Эта языкам программирования, статья, посвященная незавершена . Вы можете помочь Википедии, расширив ее .

[1] Гуттаг, Джон В.; Хорнинг, Джеймс Дж. (1993). Larch: Языки и инструменты для формальной спецификации (PDF) . Спрингер-Верлаг . ISBN 978-1-4612-2704-5 .

[1]