Здравствуйте!

В одном проекте большие трудности со спецификацией — в документах много неточностей, поэтому я вот уже неделю не пргограммирую, а пишу письма и шлифую требования.

Запарился малость и решил, что надо это проблему решать глобально.

Наткнулся на язык формальной спецификации Z.

Вопрос:

1) Кто-нибудь из присутствующих знает книгу (введение в Z), которая лучше Formal Specification and Documentation using Z: A Case Study Approach Джонатана Боуэна (Jonathan Bowen) ?

2) Кто-нибудь из присутствующих когда-либо использовал методы подобные Z в реальной работе? Если да — какие?

Заранее спасибо

Дмитрий

ДП>Вопрос:
ДП>1) Кто-нибудь из присутствующих знает книгу (введение в Z), которая лучше Formal Specification and Documentation using Z: A Case Study Approach Джонатана Боуэна (Jonathan Bowen) ?

Из заграничных книг я читал только Formal methods господина Monin.

Это галопом по Европам по всем формальным методам.

ДП>2) Кто-нибудь из присутствующих когда-либо использовал методы подобные Z в реальной работе? Если да — какие?

Система наподобие Z с выводом типов находится в любом языке семейства ML. Из наиболее распространенных: OCaml и Haskell.

Вполне можно написать прототип на любом из этих языков, который будет служить выполняемой спецификацией. Причем, необходимое для выполнение этой работы подмножество будет очень малым.

Если возникнут вопросы по этим двум языкам, то здесь наверняка найдутся люди (и я в том числе), которые смогут ответить.

Здравствуйте, thesz!

Спасибо за ответ!

ДП>>Вопрос:
ДП>>1) Кто-нибудь из присутствующих знает книгу (введение в Z), которая лучше Formal Specification and Documentation using Z: A Case Study Approach Джонатана Боуэна (Jonathan Bowen) ?

T>Из заграничных книг я читал только Formal methods господина Monin.

А из наших?

ДП>>2) Кто-нибудь из присутствующих когда-либо использовал методы подобные Z в реальной работе? Если да — какие?

T>Система наподобие Z с выводом типов находится в любом языке семейства ML. Из наиболее распространенных: OCaml и Haskell.

T>Вполне можно написать прототип на любом из этих языков, который будет служить выполняемой спецификацией. Причем, необходимое для выполнение этой работы подмножество будет очень малым.

С Хаскеллом я знаком.

Предположим, я написал спецификацию на Хаскелле и хочу автоматически проверить её (выявить ошибки).

Как это конкретно сделать в GHC?

Заранее благодарен

Дмитрий

T>>Из заграничных книг я читал только Formal methods господина Monin.
ДП>А из наших?

Увы, ни одной.

T>>Вполне можно написать прототип на любом из этих языков, который будет служить выполняемой спецификацией. Причем, необходимое для выполнение этой работы подмножество будет очень малым.
ДП>С Хаскеллом я знаком.
ДП>Предположим, я написал спецификацию на Хаскелле и хочу автоматически проверить её (выявить ошибки).
ДП>Как это конкретно сделать в GHC?

Проверяльщиком типов.

Мы классифицируем объекты предметной области путем создания алгебраических типов, а затем пишем над ними функции, которые производят нужные нам вычисления.

Правильно согласованные вычисления пройдут проверку выводом типов (то есть, в логике вывода типов GHC (это называется System F, по-моему) ваша модель будет считаться верной).

Модель получится функциональной — по вычислению будет создаваться новый экземпляр объекта.

Если с этой моделью все понятно, то на ссылках (IORef) можно сделать императивную модель (или какую-то еще, на потоках, например). Короче, ввести какую-то динамику.

Как-то так.

ДП>С Хаскеллом я знаком.
ДП>Предположим, я написал спецификацию на Хаскелле и хочу автоматически проверить её (выявить ошибки).
ДП>Как это конкретно сделать в GHC?

Вот, понял, как объяснить по-понятней.

Наша абстрактная спецификация — это алгебраические типы (классификация предметной области) и сигнатуры типов функций на верхнем уровне.

data ImportantObjects = O | A | I | Y

data UnimportandObjects = P | Q | R | S ImportandObjects

type MultiSet a = [a]

f1 :: MultiSet UnimportandObjects -> ImportantObject
f1 = undefined

Здесь много не проверишь, наверное, опечатки, разве, что.

Наша выполняемая спецификация — это когда задан код всех функций.

В этом случае мы проверяем исполняемую спецификацию на соответствие абстрактной и ловим ошибки в абстрактной — а вдруг функцию заданного типа мы построить не можем?

f1 :: MultiSet UnimportandObjects -> ImportantObject
f1 [] = P
f1 [S x] = x
f1 _ = ???

Вот что надо подставить в вопросики?

Вопрос риторический, конечно. Но все равно ясно, что тип для f1 написан неправильно.

Здравствуйте, thesz, Вы писали:

[]

T>Если с этой моделью все понятно, то на ссылках (IORef) можно сделать императивную модель (или какую-то еще, на потоках, например). Короче, ввести какую-то динамику.

Попался!

T>Как-то так.

T>>Если с этой моделью все понятно, то на ссылках (IORef) можно сделать императивную модель (или какую-то еще, на потоках, например). Короче, ввести какую-то динамику.

КЛ>Попался!

В смысле?

Моему визави нужна, скорее всего, модель для большого проекта на чем-нибудь императивном.

Вот я и предлагаю смоделировать эту самую императивщину на языке полегче.

Здравствуйте!

Если я всё-таки хочу написать спецификацию системы на Z, в каком редакторе это можно сделать?

Я пробовал jEdit вместе с CZT, но их шрифт для Z ломает мне .NET (см. здесь).

Какие есть возможности, кроме TeX?

Заранее спасибо

Дмитрий

ДП>Какие есть возможности, кроме TeX?

Не знаю.

Для Хаскеля есть lhs2tex, мощная система.