File: Chap2.mod

package info (click to toggle)
cafeobj 1.6.0-2
  • links: PTS, VCS
  • area: main
  • in suites: bookworm, bullseye, sid
  • size: 19,900 kB
  • sloc: lisp: 85,055; sh: 659; makefile: 437; perl: 147
file content (17 lines) | stat: -rw-r--r-- 303 bytes parent folder | download | duplicates (4) 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
 
module STORE {
  pr (ZZ)
  pr (Id * { sort Id -> Var })
  signature {
    [ Store ]
    op _[[_]] : Store Var -> Int
    op _;_:=_ : Store Var Var -> Store
  }
  axioms {
    vars X Y Z  : Var
    var S : Store
    eq S ; X := Y [[X]] = S [[Y]] .
    cq S ; X := Y [[Z]] = S [[Z]] if X =/= Z .
  }
}