Это команда alt-ergo, которую можно запустить в бесплатном хостинг-провайдере OnWorks, используя одну из наших многочисленных бесплатных онлайн-рабочих станций, таких как Ubuntu Online, Fedora Online, онлайн-эмулятор Windows или онлайн-эмулятор MAC OS.
ПРОГРАММА:
ИМЯ
Alt-Ergo - автоматическое средство доказательства теорем, предназначенное для проверки программ.
СИНТАКСИС
альт-эрго [ кредита ] файл
ОПИСАНИЕ
Альт-Эрго является автоматическим средством доказательства теорем. Он принимает в качестве входных данных произвольный полиморфный и
Написанная многосортная формула первого порядка имеет такой синтаксис.
ДОПОЛНИТЕЛЬНЫЕ ОПЦИИ
-h Помощь. Дает вам полный список параметров командной строки.
ПРИМЕРЫ
Теория функциональных массивов с целочисленными индексами. Эта теория предоставляет встроенный тип
('a,' b) farray и встроенный синтаксис для управления массивами.
Например, учитывая абстрактный тип данных tau и функциональный массив t типа (int,
tau) farray заявил следующее:
тип тау
логика t: (int, tau) farray
Выражения:
t [i] обозначает значение, хранящееся в t по индексу i
t [i1 <-v1, ..., in <-vn] обозначает массив, который хранит те же значения, что и t для каждого
index, кроме, возможно, i1, ..., in, где хранятся значения v1, ..., vn. Это выражение
эквивалентно ((t [i1 <-v1]) [i2 <-v2]) ... [in <-vn].
Примеры.
t [0 <-v] [1 <-w]
t [0 <-v, 1 <-w]
t [0 <-v, 1 <-w] [1]
Теория перечислительных типов.
Например, тип перечисления t с конструкторами A, B, C определяется следующим образом
:
введите t = A | B | C
Это означает, что все значения типа t равны A, B или C. И что все
эти конструкторы разные.
Теория полиморфных записей.
Например, полиморфная запись типа 'at с двумя метками a и b типа' a и
int соответственно определяется следующим образом:
введите 'at = {a:' a; b: int}
Выражения {a = 4; b = 5} и {r с b = 3} обозначают записи, а точка
обозначение ra используется для доступа к меткам.
Alt-Ergo (v.> = 0.95) позволяет пользователю указать тип терминов, используя синтаксис :
. Пример ниже иллюстрирует использование этой новой функции.
введите список
логический ноль: 'b список
логика f: 'c list -> int
цель g1: f (nil) = f (nil) (* недействительно, потому что два экземпляра nil могут иметь
различные виды *)
цель g2: f (nil: 'd list) = f (nil:' d list) (* действительно *)
ОКРУЖАЮЩАЯ СРЕДА ПЕРЕМЕННЫЕ
ЭРГОЛИБ
Альтернативный путь к библиотеке Alt-Ergo
АВТОРЫ
Сильвен Коншон <conchon@lri.fr> и Эвелин Контеджан <contextjea@lri.fr>
Используйте alt-ergo онлайн с помощью сервисов onworks.net