Лиственница Прувер

The Larch Prover , или LP сокращенно , представляет собой интерактивную систему доказательства теорем для многосортной логики первого порядка . В 1990-х годах его использовали в Массачусетском технологическом институте и других местах для рассуждений о проектировании схем , параллельных алгоритмов , аппаратного и программного обеспечения. ^[1]

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

Разработка

LP был разработан Стивеном Гарландом и Джоном Гуттагом в Лаборатории компьютерных наук Массачусетского технологического института при содействии Джеймса Хорнинга и Джеймса Сакса из Исследовательского центра систем DEC в рамках проекта Larch по формальным спецификациям . ^[2] эквациональных термов REVE 2, Он расширил систему переписывания разработанную Пьером Лесканом. ^[3] Рэнди Форгаард ^[4] при содействии Дэвида Детлефса и Кэтрин Йелик . Он поддерживает доказательства путем переписывания эквациональных терминов (для терминов с ассоциативно-коммутативными операторами), случаев, противоречий, индукции, обобщения и специализации.

LP был написан на языке программирования CLU .

Пример аксиоматизации ЛП

declare sorts E, Sdeclare variables e, e1, e2: E, x, y, z: Sdeclare operators  {}:                   -> S  {__}:            E    -> S  insert:          E, S -> S  __ \union __:    S, S -> S  __ \in __:       E, S -> Bool  __ \subseteq __: S, S -> Bool  ..set name setAxiomsassert  sort S generated by {}, insert;  {e} = insert(e, {});  ~(e \in {});  e \in insert(e1, x) <=> e = e1 \/ e \in x;  {} \subseteq x;  insert(e, x) \subseteq y <=> e \in y /\ x \subseteq y;  e \in (x \union y) <=> e \in x \/ e \in y  ..set name extensionalityassert \A e (e \in x <=> e \in y) => x = y

Примеры доказательств LP

set name setTheoremsprove e \in {e}qedprove \E x \A e (e \in x <=> e = e1 \/ e = e2)  resume by specializing x to insert(e2, {e1})qed% Three theorems about union (proved using extensionality)prove x \union {} = x  instantiate y by x \union {} in extensionalityqedprove x \union insert(e, y) = insert(e, x \union y)  resume by contradiction    set name lemma    critical-pairs *Hyp with extensionalityqedprove ac \union    resume by contradiction      set name lemma      critical-pairs *Hyp with extensionality    resume by contradiction      set name lemma      critical-pairs *Hyp with extensionalityqed% Three theorems about subsetset proof-methods =>, normalizationprove e \in x /\ x \subseteq y => e \in y by induction on x      resume by case ec = e1c        set name lemma        completeqedprove x \subseteq y /\ y \subseteq x => x = y    set name lemma    prove e \in xc <=> e \in yc by <=>        complete        complete    instantiate x by xc, y by yc in extensionalityqedprove (x \union y) \subseteq z <=> x \subseteq z /\ y \subseteq z by induction on xqed% An alternate induction ruleprove sort S generated by {}, {__}, \union    set name lemma    resume by induction      critical-pairs *GenHyp with *GenHyp      critical-pairs *InductHyp with lemmaqed

Библиография

Паскаль Андре, Аня Романчук, Жан-Клод Ройе и Алин Васконселос, «Проверка согласованности UMLдиаграммы классов с использованием Larch Prover», Труды Международной конференции 2000 года по строгим объектно-ориентированным методам ,стр. 1, Йорк, Великобритания, BCS Learning & Development Ltd., Суиндон, Великобритания, январь 2000 г.

Бутейна Четали, «Формальная проверка параллельных программ с использованием Larch Prover», IEEE Transactions on Software Engineering 24:1, страницы 46–62, январь 1998 г. doi: 10.1109/32.663997.

Манфред Брой, «Опыт спецификации и проверки программного обеспечения с использованием LP, помощника по проверке Larch», Формальные методы проектирования систем 8:3, страницы 221–272, 1996.

Урбан Энгберг, Питер Грённинг и Лесли Лэмпорт, «Механическая верификация параллельных систем с помощью TLA», Компьютерная проверка , редакторы Г. В. Бохман и Д. К. Пробст, Труды четвертой международной конференции CAV'92), Конспекты лекций по информатике 663, Springer-Verlag, июнь 1992 г., страницы 44–55.

Урбан Энгберг, Рассуждения во временной логике действий , Серия диссертаций БРИКС DS 96–1,Кафедра компьютерных наук, Орхусский университет, Дания, август 1996 г. ISSN 1396-7002.

Стивен Дж. Гарланд и Джон В. Гуттаг, «Индуктивные методы рассуждений об абстрактных типах данных», Пятнадцатый ежегодный симпозиум ACM по принципам языков программирования , страницы 219–228, Сан-Диего, Калифорния, январь 1988 г.

Стивен Дж. Гарланд и Джон В. Гуттаг, «LP: The Larch Prover», Девятая международная конференция по конспектам лекций по автоматизированной дедукции по информатике , стр. 748–749, Аргонн, Иллинойс, май 1988 г. Springer-Verlag.

Стивен Дж. Гарланд, Джон В. Гуттаг и Йорген Стаунструп, «Верификация схем СБИС с использованием LP». The Fusion of Hardware Design and Verification , страницы 329–345, Глазго, Шотландия, 4–6 июля 1988 г. IFIP WG 10.2, Северная Голландия.

Стивен Дж. Гарланд и Джон В. Гуттаг, «Обзор LP, The Larch Prover», Третья международная конференция по методам и приложениям переписывания лекций по информатике 355, страницы 137–151, Чапел-Хилл, Северная Каролина, апрель 1989 г. Springer-Verlag.

Стивен Дж. Гарланд и Джон В. Гуттаг, «Использование LP для отладки спецификаций», Концепции и методы программирования , Галилейское море, Израиль, 2–5 апреля 1990 г.ИФИП РГ 2.2/2.3, Северная Голландия.

Стивен Дж. Гарланд и Джон В. Гуттаг, Путеводитель по LP: Испытатель лиственницы ,Лаборатория компьютерных наук Массачусетского технологического института, декабрь 1991 г.Также опубликовано как Отчет 82 Центра системных исследований Digital Equipment Corporation, 1991 г.

Виктор Лучанко, Экрем Сойлемез, Стивен Гарланд и Нэнси Линч,«Проверка временных свойств параллельных алгоритмов», FORTE '94: Седьмая международная конференция по методам формального описания ,страницы 259–273, Берн, Швейцария, 4–7 октября 1994 г. Chapman & Hall.

Урсула Мартин и Майкл Лай, «Некоторые эксперименты с средством доказательства теоремы о пополнении», Журнал символических вычислений 13:1, 1992, страницы 81–100, ISSN 0747-7171.

Урсула Мартин и Жаннетт М. Винг, редакторы, Первый международный семинар по лиственнице ,Материалы Первого международного семинара без лиственницы, Дедхэм, Массачусетс, 13–15 июля 1992 г.,Семинары по информатике, Springer-Verlag, 1992.

Мишель Бидуа и Рольф Хенникер, «Как доказать теоремы наблюдения с помощью LP», страницы 18–35.
Бутена Четали и Пьер Лескан, «Упражнение в LP: доказательство невосстанавливающейся схемы деления», страницы 55–68.
Кристин Чоппи и Мишель Бидуа, «Интеграция ASSPEGIQUE и LP», страницы 69–85.
Нильс Меллергаард и Йорген Стаунструп, «Формирование обязательств по доказательству для схем», страницы 185–200.
Э.А. Скотт и К.Дж. Норри, «Использование LP для изучения языка PL _0».⁺", страницы 227–245.
Фредерик Вуазен, «Новый интерфейс для прувера из лиственницы», страницы 282–296.
Дж. М. Винг, Э. Роллинз и А. Мурман Заремски, «Мысли о лиственнице/ML и новом приложении для LP», страницы 297–312.

То Не Вин, Майкл Д. Эрнст, Стивен Дж. Гарланд, Дилсун Кирли и Нэнси Линч,Использование моделирования выполнения при проверке распределенных алгоритмов». Программные средства для передачи технологий 6:1, Ленор Д. Цук , Пол С. Этти,Агостино Кортези и Супратик Мухопадьяй (редакторы), страницы 67–76. Спрингер-Верлаг, июль 2004 г.

Цветомир П. Петров, Аня Погосянц, Стивен Дж. Гарланд, Виктор Лучанко и Нэнси А. Линч,«Компьютерная проверка алгоритма для одновременных меток времени». Методы формального описания IX: Теория, применение и инструменты (FORTE/PSTV) ,Рейнхард Готцхейн и Ян Бредереке (редакторы), страницы 29–44, Кайзерслаутерн, Германия, 8–11 октября 1996 г. Chapman & Hall.

Джеймс Б. Сакс, Стивен Дж. Гарланд, Джон В. Гуттаг и Джеймс Дж. Хорнинг,«Использование преобразований и проверок в схемотехнике», Формальные методы проектирования систем 3:3 (декабрь 1993 г.), страницы 181–209.

Йорген Ф. Согаард-Андерсон, Стивен Дж. Гарланд, Джон В. Гуттаг, Нэнси А. Линч и Аня Погосянц,«Доказательства с помощью компьютерного моделирования», Пятая конференция по компьютерной верификации (CAV '03) ,Костас Куркубетис (редактор), Конспекты лекций по информатике 697, страницы 305–319, Элунда, Греция, июнь 1993 г. Springer-Verlag.

Йорген Стаунструп, Стивен Дж. Гарланд и Джон В. Гуттаг,«Локальная проверка описаний схем», Методы автоматической верификации для систем с конечным состоянием , Конспект лекций по информатике 407,страницы 349–364, Гренобль, Франция, июнь 1989 г. Springer-Verlag.

Йорген Стаунструп, Стивен Дж. Гарланд и Джон В. Гуттаг,«Механизированная проверка описаний схем с помощью Лиственничного прувера», «Доказательства теорем в схемотехнике» , Виктория Ставриду, Томас Ф. Мелхэм и Рэймонд Т. Баут (редакторы), IFIP Transactions A-10 , страницы 277–299, Неймеген, Нидерланды, 22–24 июня 1992 г. Северная Голландия.

Марк Т. Вандевурде и Дипак Капур, «Распределенный прувер Larch (DLP): эксперимент по распараллеливанию прувера на основе правил перезаписи», Международная конференция по методам и приложениям перезаписи RTA 1996 , Конспекты лекций по информатике 1103, страницы 420–423. Спрингер-Верлаг.

Фредерик Вуазен, «Новый менеджер доказательств и графический интерфейс для прувера Larch», Международная конференция по методам и приложениям перезаписи RTA 1996 , Конспекты лекций по информатике 1103, страницы 408–411. Спрингер-Верлаг.

Жанетт М. Винг и Чун Гонг, Опыт работы с прувером из лиственницы, Заметки по разработке программного обеспечения ACM SIGSOFT 15:44, сентябрь 1990 г.,страницы 140–143 https://doi.org/10.1145/99571.99835

Ссылки

^ 1985 Исследование лиственницы, Университет Чарнеги-Меллон.
^ Джон В. Гуттаг и Джеймс Хорнинг с С. Дж. Гарландом, К. Д. Джонсом, А. Модетом и Дж. М. Вингом, Лиственница: языки и инструменты для формальной спецификации , Тексты и монографии Springer-Verlag в области компьютерных наук, 1993. ISBN 978-1-4612 -2704-5.
^ Пьер Лесканн и «Компьютерные эксперименты с генератором системы переписывания терминов REVE», Труды 10-го симпозиума ACM SIGACT-SIGPLAN по принципам языков программирования , POPL '83, Остин, Техас, Ассоциация вычислительной техники, Нью-Йорк, Нью-Йорк, страницы 99–108.
^ Рэнди Форгаард и Джон Гуттаг, «REVE: генератор системы переписывания терминов с отказоустойчивым Кнут-Бендиксом», Труды семинара по переписыванию терминов , под редакцией Д. Капура и Д. Массера, апрель 1984 г., страницы 5–31 .

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

[1] 1985 Исследование лиственницы, Университет Чарнеги-Меллон.

[2] Джон В. Гуттаг и Джеймс Хорнинг с С. Дж. Гарландом, К. Д. Джонсом, А. Модетом и Дж. М. Вингом, Лиственница: языки и инструменты для формальной спецификации , Тексты и монографии Springer-Verlag в области компьютерных наук, 1993. ISBN 978-1-4612 -2704-5.

[3] Пьер Лесканн и «Компьютерные эксперименты с генератором системы переписывания терминов REVE», Труды 10-го симпозиума ACM SIGACT-SIGPLAN по принципам языков программирования , POPL '83, Остин, Техас, Ассоциация вычислительной техники, Нью-Йорк, Нью-Йорк, страницы 99–108.

[4] Рэнди Форгаард и Джон Гуттаг, «REVE: генератор системы переписывания терминов с отказоустойчивым Кнут-Бендиксом», Труды семинара по переписыванию терминов , под редакцией Д. Капура и Д. Массера, апрель 1984 г., страницы 5–31 .

[1]

[2]

[3]

[4]