summaryrefslogtreecommitdiff
path: root/Binaries/UnivBackPred2.sx
blob: 7c3dac8ed525ac2443b8bc6834cf32c8a9179960 (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
; -------------------------------------------------------------------------
; 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)))

))  ;; AND, BG_PUSH
; End Boogie universal background predicate
; -------------------------------------------------------------------------