54 lines
1.2 KiB
Plaintext
54 lines
1.2 KiB
Plaintext
|
; ----------------------------------------------------------------------
|
||
|
|
; Boogie universal background predicate
|
||
|
|
; Copyright (c), Microsoft Corp.
|
||
|
|
(&&
|
||
|
|
; select/store axioms, 1 index argument
|
||
|
|
|
||
|
|
(forall (A i v)
|
||
|
|
(= (select1 (store1 A i v) i) v))
|
||
|
|
|
||
|
|
(forall (A i j v)
|
||
|
|
(==> (!= i j)
|
||
|
|
(=
|
||
|
|
(select1 (store1 A i v) j)
|
||
|
|
(select1 A j))))
|
||
|
|
|
||
|
|
; select/store axioms, 2 index arguments
|
||
|
|
|
||
|
|
(forall (A o f v)
|
||
|
|
(= (select2 (store2 A o f v) o f) v))
|
||
|
|
|
||
|
|
(forall (A o f p g v)
|
||
|
|
(==> (!= o p)
|
||
|
|
(=
|
||
|
|
(select2 (store2 A o f v) p g)
|
||
|
|
(select2 A p g))))
|
||
|
|
|
||
|
|
(forall (A o f p g v)
|
||
|
|
(==> (!= f g)
|
||
|
|
(=
|
||
|
|
(select2 (store2 A o f v) p g)
|
||
|
|
(select2 A p g))))
|
||
|
|
|
||
|
|
; <: is a partial order: it is reflexive, transitive, and anti-symmetric
|
||
|
|
|
||
|
|
(forall (t)
|
||
|
|
(<: t t)
|
||
|
|
(PATS (<: t t)))
|
||
|
|
|
||
|
|
(forall (t u v)
|
||
|
|
(==>
|
||
|
|
(&& (<: t u ) (<: u v))
|
||
|
|
(<: t v))
|
||
|
|
(PATS (MPAT (= (<: t u) true) (= (<: u v) true))))
|
||
|
|
|
||
|
|
(forall (t u)
|
||
|
|
(==>
|
||
|
|
(&& (<: t u) (<: u t))
|
||
|
|
(= t u))
|
||
|
|
(PATS (MPAT (<: t u) (<: u t))))
|
||
|
|
|
||
|
|
)
|
||
|
|
; End Boogie universal background predicate
|
||
|
|
; ----------------------------------------------------------------------
|