これは、Ubuntu Online、Fedora Online、Windows オンライン エミュレーター、MAC OS オンライン エミュレーターなど、複数の無料オンライン ワークステーションのいずれかを使用して、OnWorks 無料ホスティング プロバイダーで実行できるコマンド cafeobj です。
プログラム：
NAME
cafeobj - 代数仕様とプログラミング言語
SYNOPSIS
カフェオブジェクト [オプション] ... [ファイル] ...
DESCRIPTION
を開始します カフェOBJ 通訳。
カフェOBJ 多くの先進技術を継承した最先端の形式仕様言語
機能 (例: 柔軟な mix-fix 構文、順序付きの強力で明確なタイピング システム
並べ替え、パラメーターをインスタンス化するためのパラメーター モジュールとビュー、およびモジュール
式など) OBJ (より正確には OBJ3) 代数仕様言語から。
CafeOBJ は、モデルの正式な (つまり数学的) 仕様を記述するための言語です。
多種多様なソフトウェアやシステムを開発し、それらの特性を検証します。 カフェOBJ
書き換えによって等式論理を実装し、強力な対話型定理として使用できます
証明系。 指定子は、CafeOBJ でも証明スコアを書き、次の方法で証明できます。
証明スコアを実行します。
CafeOBJ は、制度に基づく最先端の厳密な論理セマンティクスを備えています。 カフェOBJ
キューブは、さまざまなロジックの組み合わせの基礎となるさまざまなロジックの構造を示しています。
言語によって実装されるパラダイム。 CafeOBJ のプルーフ スコアも以下に基づいています。
制度ベースの厳密なセマンティクスであり、完全な証明セットを使用して構築できます
ルール。
OPTIONS
オプションには XNUMX つのクラスがあります。 最初のオプションは、 カフェオブジェクト ラッパースクリプト
基礎となる Common Lisp インタープリターを選択し、検索パスを調整することができます
パラメーター。
-エンジン NAME
基礎となる Common Lisp エンジンを選択します。 指定されていない場合は、最初に選択されたもの
ビルド時に使用されます。
-リストエンジン
利用可能なすべての一般的な Lisp エンジンを一覧表示します
-wrapper-libpath パス
Lisp インタプリタのメモリ ダンプが見つかるパスを設定します
-ラッパー共有パス パス
CafeOBJ 初期化ファイルが検索されるパスを設定します
次の一連のオプションは、CafeOBJ インタープリターに直接向けられます。
-助けて ヘルプメッセージを印刷する
-q ユーザーの初期化ファイルをロードしない
-バッチ バッチモードで実行
-p パス
モジュールを定義する標準プレリュードファイルを与える
+p パス
追加のプレリュード ファイルを読み込む
-l DIR リスト
コロンで区切られた、モジュール検索パスのパス名のリストを設定します
+l DIR リスト
モジュール検索パスのパス名のリストを追加します
ファイル 起動時に読み込まれるファイルを順番に並べます。
onworks.net サービスを使用してオンラインで cafeobj を使用する
