CspCASL/test/test.cspcasl

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
logic CspCASL

spec test =
  data {
    sort mySort < mySuper
    ops c : mySort;
    d : mySort;
    myFun : mySort -> mySuper
    pred p: mySort

    var x:mySort

    axioms myFun(c) = d;
    x = d}

  channel
    C:mySuper

  process

    A : mySuper;
    A = d -> myFun(d) -> [] x :: mySort -> x -> myFun(x) -> SKIP
end