これは、Ubuntu Online、Fedora Online、Windows オンライン エミュレーター、MAC OS オンライン エミュレーターなどの複数の無料オンライン ワークステーションの XNUMX つを使用して、OnWorks 無料ホスティング プロバイダーで実行できるコマンド alt-ergo です。
プログラム：
NAME
Alt-Ergo - プログラム検証専用の自動定理証明器
SYNOPSIS
代替エルゴ [ オプション ] file
DESCRIPTION
オルタナティブ 自動定理証明器です。 入力として任意の多態性を受け取り、
マルチソートされた一次数式は、Why のような構文で記述されます。
OPTIONS
-h ヘルプ。 コマンドラインオプションの完全なリストが表示されます。
例
整数インデックスを持つ関数配列の理論。 この理論は組み込み型を提供します。
('a,'b) farray と配列を操作するための組み込み構文。
たとえば、抽象データ型 tau と型 (int,
tau) farray は次のように宣言されます。
タウ型
ロジック t : (int, tau) farray
式：
t[i] は、インデックス i の t に格納されている値を示します。
t[i1<-v1,...,in<-vn] は、すべての場合に t と同じ値を格納する配列を示します。
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]
列挙型の理論。
たとえば、コンストラクター A、B、C を持つ列挙型 t は次のように定義されます。
:
タイプ t = A | B | C
これは、型 t のすべての値が A、B、または C のいずれかに等しいことを意味します。
これらのコンストラクターは別個のものです。
ポリモーフィック レコードの理論。
たとえば、型 'a および型の XNUMX つのラベル a および b を持つ多態性レコード型 'at の場合、
int はそれぞれ次のように定義されます。
type 'at = { a : 'a; b : int }
式 { a = 4; b = 5 } と { r with b = 3} はレコードを示し、ドットは
表記 ra はラベルにアクセスするために使用されます。
Alt-Ergo (v. >= 0.95) を使用すると、ユーザーは構文を使用して用語の種類を強制できます。 :
。 以下の例は、この新しい機能の使用法を示しています。
リストを入力してください
論理 nil : 'b リスト
ロジック f : 'c list -> int
目標 g1 : f(nil) = f(nil) (* nil の XNUMX つのインスタンスは
他の種類 *）
目標 g2 : f(nil:'d リスト) = f(nil:'d リスト) (* 有効 *)
ENVIRONMENT 変数
エルゴリブ
Alt-Ergo ライブラリの代替パス
作者
シルヴァン・コンション <[メール保護]> そしてエヴリン・コンテジャン <[メール保護]>
onworks.net サービスを使用してオンラインで alt-ergo を使用する
