MAJ terminée. Nous sommes passés en version 14.6.2 . Pour consulter les "releases notes" associées c'est ici :

https://about.gitlab.com/releases/2022/01/11/security-release-gitlab-14-6-2-released/
https://about.gitlab.com/releases/2022/01/04/gitlab-14-6-1-released/

gappa.drv 4.57 KB
Newer Older
MARCHE Claude's avatar
gappa    
MARCHE Claude committed
1
2
3
4
5

(* Why driver for Gappa *)

prelude "# this is a prelude for Gappa"

MARCHE Claude's avatar
MARCHE Claude committed
6
printer "gappa"
MARCHE Claude's avatar
gappa    
MARCHE Claude committed
7
8
9
filename "%f-%t-%g.gappa"

valid 0
10
unknown "no contradiction was found\\|some enclosures were not satisfied" ""
11
12
time "why3cpulimit time : %s s"
fail "Error: \\(.*\\)" "\\1"
MARCHE Claude's avatar
gappa    
MARCHE Claude committed
13

14
(*transformation "simplify_recursive_definition"*)
15
transformation "inline_trivial"
MARCHE Claude's avatar
MARCHE Claude committed
16
transformation "eliminate_builtin"
MARCHE Claude's avatar
MARCHE Claude committed
17
transformation "inline_all"
18
transformation "eliminate_definition"
MARCHE Claude's avatar
MARCHE Claude committed
19
transformation "eliminate_inductive"
20
transformation "eliminate_algebraic"
MARCHE Claude's avatar
MARCHE Claude committed
21
22
23
transformation "eliminate_if"
transformation "eliminate_let"
transformation "simplify_formula"
24
transformation "simplify_unknown_lsymbols"
25
transformation "simplify_trivial_quantification"
26
transformation "introduce_premises"
27
transformation "instantiate_predicate"
28
transformation "abstract_unknown_lsymbols"
MARCHE Claude's avatar
gappa    
MARCHE Claude committed
29
30

theory BuiltIn
31
32
  syntax type int   "int"
  syntax type real  "real"
33
  syntax predicate (=)  "dummy"
MARCHE Claude's avatar
gappa    
MARCHE Claude committed
34
35
36
37
38
39
end

theory int.Int

  prelude "# this is a prelude for Gappa integer arithmetic"

40
41
  syntax function zero "0"
  syntax function one  "1"
MARCHE Claude's avatar
gappa    
MARCHE Claude committed
42

43
44
45
46
  syntax function (+)  "(%1 + %2)"
  syntax function (-)  "(%1 - %2)"
  syntax function (*)  "(%1 * %2)"
  syntax function (-_) "(-%1)"
MARCHE Claude's avatar
gappa    
MARCHE Claude committed
47

48
49
50
51
  syntax predicate (<=) "dummy"
  syntax predicate (>=) "dummy"
  syntax predicate (<)  "dummy"
  syntax predicate (>)  "dummy"
52

53
54
55
56
  meta "gappa arith" predicate (<=), "", "<=", ">="
  meta "gappa arith" predicate (>=), "", ">=", "<="
  meta "gappa arith" predicate (<), "not ", ">=", "<="
  meta "gappa arith" predicate (>), "not ", "<=", ">="
57

58
59
60
  meta "inline : no" predicate (<=)
  meta "inline : no" predicate (>=)
  meta "inline : no" predicate (>)
61

MARCHE Claude's avatar
gappa    
MARCHE Claude committed
62
63
64
65
66
67
68
69
70
71
72
73
  remove prop CommutativeGroup.Comm.Comm
  remove prop CommutativeGroup.Assoc.Assoc
  remove prop CommutativeGroup.Unit_def
  remove prop CommutativeGroup.Inv_def
  remove prop Assoc.Assoc
  remove prop Mul_distr
  remove prop Comm.Comm
  remove prop Unitary
  remove prop Refl
  remove prop Trans
  remove prop Total
  remove prop Antisymm
74
  remove prop NonTrivialRing
Guillaume Melquiond's avatar
Guillaume Melquiond committed
75
  remove prop ZeroLessOne
MARCHE Claude's avatar
gappa    
MARCHE Claude committed
76
77
78

end

MARCHE Claude's avatar
MARCHE Claude committed
79
80
theory int.Abs

81
  syntax function abs  "| %1 |"
MARCHE Claude's avatar
MARCHE Claude committed
82
83
84

end

85
86
theory int.EuclideanDivision

87
  syntax function div "int<dn>(%1 / %2)"
88
89
90
91
92

end

theory int.ComputerDivision

93
  syntax function div "int<zr>(%1 / %2)"
94
95

end
MARCHE Claude's avatar
MARCHE Claude committed
96

MARCHE Claude's avatar
gappa    
MARCHE Claude committed
97
98
99
100
theory real.Real

  prelude "# this is a prelude for Gappa real arithmetic"

101
102
  syntax function zero "0.0"
  syntax function one  "1.0"
MARCHE Claude's avatar
gappa    
MARCHE Claude committed
103

104
105
106
107
108
109
  syntax function (+)  "(%1 + %2)"
  syntax function (-)  "(%1 - %2)"
  syntax function (*)  "(%1 * %2)"
  syntax function (/)  "(%1 / %2)"
  syntax function (-_) "(-%1)"
  syntax function inv  "(1.0 / %1)"
MARCHE Claude's avatar
gappa    
MARCHE Claude committed
110

111
112
113
114
  syntax predicate (<=) "dummy"
  syntax predicate (>=) "dummy"
  syntax predicate (<)  "dummy"
  syntax predicate (>)  "dummy"
115

116
117
118
119
  meta "gappa arith" predicate (<=), "", "<=", ">="
  meta "gappa arith" predicate (>=), "", ">=", "<="
  meta "gappa arith" predicate (<), "not ", ">=", "<="
  meta "gappa arith" predicate (>), "not ", "<=", ">="
120

121
122
123
  meta "inline : no" predicate (<=)
  meta "inline : no" predicate (>=)
  meta "inline : no" predicate (>)
Andrei Paskevich's avatar
Andrei Paskevich committed
124

MARCHE Claude's avatar
gappa    
MARCHE Claude committed
125
126
127
128
129
130
131
132
133
134
135
136
137
  remove prop CommutativeGroup.Comm.Comm
  remove prop CommutativeGroup.Assoc.Assoc
  remove prop CommutativeGroup.Unit_def
  remove prop CommutativeGroup.Inv_def
  remove prop Assoc.Assoc
  remove prop Mul_distr
  remove prop Comm.Comm
  remove prop Unitary
  remove prop Refl
  remove prop Trans
  remove prop Total
  remove prop Antisymm
  remove prop Inverse
138
  remove prop NonTrivialRing
Guillaume Melquiond's avatar
Guillaume Melquiond committed
139
  remove prop ZeroLessOne
MARCHE Claude's avatar
gappa    
MARCHE Claude committed
140
141
142

end

143
144
theory real.Abs

145
  syntax function abs  "| %1 |"
146
147
148

end

149
150
theory real.Square

151
  syntax function sqrt  "sqrt(%1)"
152
153
154

end

155
156
theory real.Truncate

157
158
159
  syntax function truncate "int<zr>(%1)"
  syntax function floor    "int<dn>(%1)"
  syntax function ceil     "int<up>(%1)"
160
161
162

end

163
164
theory real.FromInt

165
  syntax function from_int "%1"
166

167
168
169
  remove prop Zero
  remove prop One

170
171
end

172
173
174
175
176
177
178
179
180
181
theory floating_point.Rounding

  syntax function NearestTiesToEven "ne"
  syntax function ToZero "zr"
  syntax function Up "up"
  syntax function Down "dn"
  syntax function NearestTiesToAway "na"

end

182
183
theory floating_point.Single

184
  syntax function round "float<ieee_32,%1>(%2)"
185
  meta "instantiate : auto" prop Bounded_value
186
187
188

end

189
190
theory floating_point.Double

191
  syntax function round "float<ieee_64,%1>(%2)"
192
  meta "instantiate : auto" prop Bounded_value
193
194
195

end

196
197
(*
theory floating_point.SingleMultiRounding
198

199
200
  syntax function round "float<ieee_32,%1>(%2)"
  meta "instantiate : auto" prop Bounded_value
201

202
end
203
204
205
206
207
208
209
210
211
*)

theory floating_point.DoubleMultiRounding

  syntax function round "float<ieee_64,%1>(%2)"
  meta "instantiate : auto" prop Bounded_value

end

212

MARCHE Claude's avatar
gappa    
MARCHE Claude committed
213
(*
MARCHE Claude's avatar
MARCHE Claude committed
214
Local Variables:
MARCHE Claude's avatar
gappa    
MARCHE Claude committed
215
216
mode: why
compile-command: "make -C .. bench"
MARCHE Claude's avatar
MARCHE Claude committed
217
End:
MARCHE Claude's avatar
gappa    
MARCHE Claude committed
218
*)