Abstruct Machine Notation(抽象機械表記法) について

質問

こんにちわ！どなたか抽象機械表記法を使ったプログラミングに強い方おられませんか？今、大学でFormal Method　という授業を受けているのですがこれがすっかりわかりません・・・　インターネットなどでサンプルが掲載されているところや、これについて参考になるようなサイトなどありましたら教えていただけませんか？よろしくお願いします。私はこれがなんと言うプログラミング言語なのかすら解っておりません・・・　授業では”Machine readable AMN”と記載されていますが、インターネットで検索してもなかなかヒットしてくれません。
プログラムはこんな感じです↓↓↓
MACHINE sample （プログラムの名前）
VARIABLES hasread (変数定義)
SETS children = {Mike,Bill,Ken};
books = {Sugaku,Kokugo,Rika}
INVARIANT hasread : children <-> books　（不変の定義）
INITIALISATION hasread := {} (変数の初期化)
OPERATIONS　　　（操作）
record(cc,bb)=
PRE cc : children & bb : books
THEN hasread := hasread \/ {cc |-> bb}
END
END　（プログラム終了）
＜Sample.mch という拡張子のファイルができます。＞
このプログラムを使うさいに、LinuxのB-tool kitというコンパイラ（？）を使用しています。なにか解る事があれば回答お願いします。

回答No.1

noname#7858

Abstract Machine Notation（Abstruct でなく Abstract）なら、Google でいろいろ引っかかるみたいですよ。英語ページのみ。

どういう言語かは…、
抽象機械用の言語なんでしょうね、たぶん？

お礼

おっと、スペル間違えてました・・・　探してみます。ありがとうございます！！