blob: 7e30017b2e2f191336828d1d0b9c6503795b3b21 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
|
; -------------------------------------------------------------------------
; Boogie 2 universal background predicate
; Copyright (c) 2004-2008, Microsoft Corp.
(DEFPRED (<: t u)) ; used for translation with type premisses
(DEFPRED (<:: s t u)) ; used for translation with type arguments
(BG_PUSH (AND
; formula/term axioms
(FORALL (x y)
(IFF
(EQ (boolIff x y) |@true|)
(IFF (EQ x |@true|) (EQ y |@true|))))
(FORALL (x y)
(IFF
(EQ (boolImplies x y) |@true|)
(IMPLIES (EQ x |@true|) (EQ y |@true|))))
(FORALL (x y)
(IFF
(EQ (boolAnd x y) |@true|)
(AND (EQ x |@true|) (EQ y |@true|))))
(FORALL (x y)
(IFF
(EQ (boolOr x y) |@true|)
(OR (EQ x |@true|) (EQ y |@true|))))
(FORALL (x)
(PATS (boolNot x))
(IFF
(EQ (boolNot x) |@true|)
(NEQ x |@true|)))
(FORALL (x y)
(IFF
(EQ (anyEqual x y) |@true|)
(EQ x y)))
(FORALL (x y)
(PATS (anyNeq x y))
(IFF
(EQ (anyNeq x y) |@true|)
(NEQ x y)))
(FORALL (x y)
(IFF
(EQ (intLess x y) |@true|)
(< x y)))
(FORALL (x y)
(IFF
(EQ (intAtMost x y) |@true|)
(<= x y)))
(FORALL (x y)
(IFF
(EQ (intAtLeast x y) |@true|)
(>= x y)))
(FORALL (x y)
(IFF
(EQ (intGreater x y) |@true|)
(> x y)))
; false is not true
(DISTINCT |@false| |@true|)
;; The following axiom gives a way to typed produce verification conditions,
;; that is, verification conditions where the terms are typable. To use these,
;; the VCExpressionGenerator.{CastTo,CastFrom} methods must be overridden.
;; Look for USE_SORTED_LOGIC in VCGeneration/VCExpr.ssc.
; (FORALL (val T U)
; (PATS (TypeConvert (TypeConvert val T U) U T))
; (EQ (TypeConvert (TypeConvert val T U) U T) val))
; Reflect plus
(FORALL (a b) (PATS (Reflect$Add a b)) (EQ (Reflect$Add a b) (+ a b)))
(EQ (tickleBool |@false|) |@true|)
(EQ (tickleBool |@true|) |@true|)
)) ;; AND, BG_PUSH
; End Boogie universal background predicate
; -------------------------------------------------------------------------
|
