日々の流転

λ. CLEAR FILE

「CLEAR FILE」と書かれているのを見て、代数的仕様記述言語CLEARのファイル形式か何かだと一瞬思ってしまった。疲れてるな。

ちなみに、CLEARは以下のような感じの言語。

constant Triv =
    theory
        sort element
    endth

procedure Prod(A:Triv,B:Triv) =
    theory
        data sort prod
        opns pair: element of A,element of B -> prod
             pi1 : prod -> element of A
             pi2 : prod -> element of B
        eqns all a:element of A,b:element of B,
                                   pi1(pair(a,b)) = a
             all a:element of A,b:element of B,
                                   pi2(pair(a,b)) = b
    endth

この例はCPLの論文からとってきた例で、ここでは直積型の仕様を記述している。

詳しくはこの辺りの論文でもどうぞ。私は読んだことないけどね。

• Burstall, R. M. and Goguen, J. A. (1980): The Semantics of Clear: A Specification Language. Internal Report CSR-65-80, Department of Computer Science, University of Edinburgh.
• Burstall, R. M. and Goguen, J.A. (1982): Algebras, Theories and Freeness: an Introduction for Computer Scientists. Internal Report CSR-65-80, Department of Computer Science, University of Edinburgh.