Skip to content

Commit 0a62216

Browse files
github-actions[bot]github-actions[bot]
committed
1 parent 83feeaf commit 0a62216

9 files changed

Lines changed: 63 additions & 63 deletions

File tree

‎refman/tactics/cfold.html‎

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -166,25 +166,25 @@ <h2><a class="toc-backref" href="#id1" role="doc-backlink">Syntax</a><a class="h
166166
},
167167
{
168168
"goals":[
169-
"Type variables: <none>\n\n------------------------------------------------------------------------\npre = witness arg\n\n M.f \n\npost = witness res\n"
169+
"Type variables: <none>\n\n------------------------------------------------------------------------\npre = witness arg\n\n M.f \n\npost = witness res\n\n"
170170
],
171171
"message":""
172172
},
173173
{
174174
"goals":[
175-
"Type variables: <none>\n\n------------------------------------------------------------------------\npre = witness arg\n\n M.f \n\npost = witness res\n"
175+
"Type variables: <none>\n\n------------------------------------------------------------------------\npre = witness arg\n\n M.f \n\npost = witness res\n\n"
176176
],
177177
"message":""
178178
},
179179
{
180180
"goals":[
181-
"Type variables: <none>\n\n------------------------------------------------------------------------\nContext : hr: {a, x, y : int}\n\npre = witness a\n\n(1) x <- a + 1 \n(2) y <- 2 * x \n(3) x <- 3 * y \n\npost = witness x\n"
181+
"Type variables: <none>\n\n------------------------------------------------------------------------\nContext : hr: {a, x, y : int}\n\npre = witness a\n\n(1) x <- a + 1 \n(2) y <- 2 * x \n(3) x <- 3 * y \n\npost = witness x\n\n"
182182
],
183183
"message":""
184184
},
185185
{
186186
"goals":[
187-
"Type variables: <none>\n\n------------------------------------------------------------------------\nContext : hr: {a, x, y : int}\n\npre = witness a\n\n(1) y <- 2 * (a + 1) \n(2) x <- 3 * y \n\npost = witness x\n"
187+
"Type variables: <none>\n\n------------------------------------------------------------------------\nContext : hr: {a, x, y : int}\n\npre = witness a\n\n(1) y <- 2 * (a + 1) \n(2) x <- 3 * y \n\npost = witness x\n\n"
188188
],
189189
"message":""
190190
},
@@ -234,31 +234,31 @@ <h2><a class="toc-backref" href="#id1" role="doc-backlink">Syntax</a><a class="h
234234
},
235235
{
236236
"goals":[
237-
"Type variables: <none>\n\n------------------------------------------------------------------------\npre = witness\n\n M.f \n\npost = witness res\n"
237+
"Type variables: <none>\n\n------------------------------------------------------------------------\npre = witness\n\n M.f \n\npost = witness res\n\n"
238238
],
239239
"message":""
240240
},
241241
{
242242
"goals":[
243-
"Type variables: <none>\n\n------------------------------------------------------------------------\npre = witness\n\n M.f \n\npost = witness res\n"
243+
"Type variables: <none>\n\n------------------------------------------------------------------------\npre = witness\n\n M.f \n\npost = witness res\n\n"
244244
],
245245
"message":""
246246
},
247247
{
248248
"goals":[
249-
"Type variables: <none>\n\n------------------------------------------------------------------------\nContext : hr: {x, y, i : int}\n\npre = witness\n\n(1--) i <- 0 \n(2--) while (i < 10) { \n(2.1) x <- i + 1 \n(2.2) y <- 2 * x \n(2.3) x <- 3 * y \n(2.4) i <- i + 1 \n(2--) } \n\npost = witness x\n"
249+
"Type variables: <none>\n\n------------------------------------------------------------------------\nContext : hr: {x, y, i : int}\n\npre = witness\n\n(1--) i <- 0 \n(2--) while (i < 10) { \n(2.1) x <- i + 1 \n(2.2) y <- 2 * x \n(2.3) x <- 3 * y \n(2.4) i <- i + 1 \n(2--) } \n\npost = witness x\n\n"
250250
],
251251
"message":""
252252
},
253253
{
254254
"goals":[
255-
"Type variables: <none>\n\n------------------------------------------------------------------------\nContext : hr: {x, y, i : int}\n\npre = witness\n\n( 1) x <- 1 \n( 2) y <- 2 * x \n( 3) x <- 3 * y \n( 4) x <- 2 \n( 5) y <- 2 * x \n( 6) x <- 3 * y \n( 7) x <- 3 \n( 8) y <- 2 * x \n( 9) x <- 3 * y \n(10) x <- 4 \n(11) y <- 2 * x \n(12) x <- 3 * y \n(13) x <- 5 \n(14) y <- 2 * x \n(15) x <- 3 * y \n(16) x <- 6 \n(17) y <- 2 * x \n(18) x <- 3 * y \n(19) x <- 7 \n(20) y <- 2 * x \n(21) x <- 3 * y \n(22) x <- 8 \n(23) y <- 2 * x \n(24) x <- 3 * y \n(25) x <- 9 \n(26) y <- 2 * x \n(27) x <- 3 * y \n(28) x <- 10 \n(29) y <- 2 * x \n(30) x <- 3 * y \n(31) i <- 10 \n\npost = witness x\n"
255+
"Type variables: <none>\n\n------------------------------------------------------------------------\nContext : hr: {x, y, i : int}\n\npre = witness\n\n( 1) x <- 1 \n( 2) y <- 2 * x \n( 3) x <- 3 * y \n( 4) x <- 2 \n( 5) y <- 2 * x \n( 6) x <- 3 * y \n( 7) x <- 3 \n( 8) y <- 2 * x \n( 9) x <- 3 * y \n(10) x <- 4 \n(11) y <- 2 * x \n(12) x <- 3 * y \n(13) x <- 5 \n(14) y <- 2 * x \n(15) x <- 3 * y \n(16) x <- 6 \n(17) y <- 2 * x \n(18) x <- 3 * y \n(19) x <- 7 \n(20) y <- 2 * x \n(21) x <- 3 * y \n(22) x <- 8 \n(23) y <- 2 * x \n(24) x <- 3 * y \n(25) x <- 9 \n(26) y <- 2 * x \n(27) x <- 3 * y \n(28) x <- 10 \n(29) y <- 2 * x \n(30) x <- 3 * y \n(31) i <- 10 \n\npost = witness x\n\n"
256256
],
257257
"message":""
258258
},
259259
{
260260
"goals":[
261-
"Type variables: <none>\n\n------------------------------------------------------------------------\nContext : hr: {x, y, i : int}\n\npre = witness\n\n( 1) y <- 2 \n( 2) y <- 4 \n( 3) y <- 6 \n( 4) y <- 8 \n( 5) y <- 10 \n( 6) y <- 12 \n( 7) y <- 14 \n( 8) y <- 16 \n( 9) y <- 18 \n(10) x <- 10 \n(11) y <- 2 * x \n(12) x <- 3 * y \n(13) i <- 10 \n\npost = witness x\n"
261+
"Type variables: <none>\n\n------------------------------------------------------------------------\nContext : hr: {x, y, i : int}\n\npre = witness\n\n( 1) y <- 2 \n( 2) y <- 4 \n( 3) y <- 6 \n( 4) y <- 8 \n( 5) y <- 10 \n( 6) y <- 12 \n( 7) y <- 14 \n( 8) y <- 16 \n( 9) y <- 18 \n(10) x <- 10 \n(11) y <- 2 * x \n(12) x <- 3 * y \n(13) i <- 10 \n\npost = witness x\n\n"
262262
],
263263
"message":""
264264
},

‎refman/tactics/hoare-split.html‎

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -155,32 +155,32 @@ <h2><a class="toc-backref" href="#id2" role="doc-backlink">Example</a><a class="
155155
},
156156
{
157157
"goals":[
158-
"Type variables: <none>\n\nn: int\n------------------------------------------------------------------------\n0 <= n => hoare[ M.incr : arg = n ==> n < res /\\ 0 <= res]\n"
158+
"Type variables: <none>\n\nn: int\n------------------------------------------------------------------------\n0 <= n => hoare[ M.incr : arg = n ==> n < res /\\ 0 <= res ]]\n"
159159
],
160160
"message":""
161161
},
162162
{
163163
"goals":[
164-
"Type variables: <none>\n\nn: int\n------------------------------------------------------------------------\n0 <= n => hoare[ M.incr : arg = n ==> n < res /\\ 0 <= res]\n"
164+
"Type variables: <none>\n\nn: int\n------------------------------------------------------------------------\n0 <= n => hoare[ M.incr : arg = n ==> n < res /\\ 0 <= res ]]\n"
165165
],
166166
"message":""
167167
},
168168
{
169169
"goals":[
170-
"Type variables: <none>\n\nn: int\nge0_n: 0 <= n\n------------------------------------------------------------------------\nContext : hr: {x, y : int}\n\npre = x = n\n\n(1) y <- x + 1 \n\npost = n < y /\\ 0 <= y\n"
170+
"Type variables: <none>\n\nn: int\nge0_n: 0 <= n\n------------------------------------------------------------------------\nContext : hr: {x, y : int}\n\npre = x = n\n\n(1) y <- x + 1 \n\npost = n < y /\\ 0 <= y\n\n"
171171
],
172172
"message":""
173173
},
174174
{
175175
"goals":[
176-
"Type variables: <none>\n\nn: int\nge0_n: 0 <= n\n------------------------------------------------------------------------\nContext : hr: {x, y : int}\n\npre = x = n\n\n(1) y <- x + 1 \n\npost = 0 <= y\n",
177-
"Type variables: <none>\n\nn: int\nge0_n: 0 <= n\n------------------------------------------------------------------------\nContext : hr: {x, y : int}\n\npre = x = n\n\n(1) y <- x + 1 \n\npost = n < y\n"
176+
"Type variables: <none>\n\nn: int\nge0_n: 0 <= n\n------------------------------------------------------------------------\nContext : hr: {x, y : int}\n\npre = x = n\n\n(1) y <- x + 1 \n\npost = 0 <= y\n\n",
177+
"Type variables: <none>\n\nn: int\nge0_n: 0 <= n\n------------------------------------------------------------------------\nContext : hr: {x, y : int}\n\npre = x = n\n\n(1) y <- x + 1 \n\npost = n < y\n\n"
178178
],
179179
"message":""
180180
},
181181
{
182182
"goals":[
183-
"Type variables: <none>\n\nn: int\nge0_n: 0 <= n\n------------------------------------------------------------------------\nContext : hr: {x, y : int}\n\npre = x = n\n\n(1) y <- x + 1 \n\npost = n < y\n"
183+
"Type variables: <none>\n\nn: int\nge0_n: 0 <= n\n------------------------------------------------------------------------\nContext : hr: {x, y : int}\n\npre = x = n\n\n(1) y <- x + 1 \n\npost = n < y\n\n"
184184
],
185185
"message":""
186186
},

‎refman/tactics/if.html‎

Lines changed: 10 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -157,52 +157,52 @@ <h2><a class="toc-backref" href="#id1" role="doc-backlink">Variant: <code class=
157157
},
158158
{
159159
"goals":[
160-
"Type variables: <none>\n\n------------------------------------------------------------------------\npre = p tt\n\n M.f \n\npost = 0 <= res\n"
160+
"Type variables: <none>\n\n------------------------------------------------------------------------\npre = p tt\n\n M.f \n\npost = 0 <= res\n\n"
161161
],
162162
"message":""
163163
},
164164
{
165165
"goals":[
166-
"Type variables: <none>\n\n------------------------------------------------------------------------\npre = p tt\n\n M.f \n\npost = 0 <= res\n"
166+
"Type variables: <none>\n\n------------------------------------------------------------------------\npre = p tt\n\n M.f \n\npost = 0 <= res\n\n"
167167
],
168168
"message":""
169169
},
170170
{
171171
"goals":[
172-
"Type variables: <none>\n\n------------------------------------------------------------------------\nContext : hr: {x, y : int}\n\npre = p tt\n\n(1--) if (x < 0) { \n(1.1) y <- -x \n(1--) } else { \n(1?1) y <- x \n(1--) } \n\npost = 0 <= y\n"
172+
"Type variables: <none>\n\n------------------------------------------------------------------------\nContext : hr: {x, y : int}\n\npre = p tt\n\n(1--) if (x < 0) { \n(1.1) y <- -x \n(1--) } else { \n(1?1) y <- x \n(1--) } \n\npost = 0 <= y\n\n"
173173
],
174174
"message":""
175175
},
176176
{
177177
"goals":[
178-
"Type variables: <none>\n\n------------------------------------------------------------------------\nContext : hr: {x, y : int}\n\npre = p tt /\\ x < 0\n\n(1) y <- -x \n\npost = 0 <= y\n",
179-
"Type variables: <none>\n\n------------------------------------------------------------------------\nContext : hr: {x, y : int}\n\npre = p tt /\\ ! x < 0\n\n(1) y <- x \n\npost = 0 <= y\n"
178+
"Type variables: <none>\n\n------------------------------------------------------------------------\nContext : hr: {x, y : int}\n\npre = p tt /\\ x < 0\n\n(1) y <- -x \n\npost = 0 <= y\n\n",
179+
"Type variables: <none>\n\n------------------------------------------------------------------------\nContext : hr: {x, y : int}\n\npre = p tt /\\ ! x < 0\n\n(1) y <- x \n\npost = 0 <= y\n\n"
180180
],
181181
"message":""
182182
},
183183
{
184184
"goals":[
185-
"Type variables: <none>\n\n------------------------------------------------------------------------\nContext : hr: {x, y : int}\n\npre = p tt /\\ x < 0\n\n\npost = 0 <= -x\n",
186-
"Type variables: <none>\n\n------------------------------------------------------------------------\nContext : hr: {x, y : int}\n\npre = p tt /\\ ! x < 0\n\n(1) y <- x \n\npost = 0 <= y\n"
185+
"Type variables: <none>\n\n------------------------------------------------------------------------\nContext : hr: {x, y : int}\n\npre = p tt /\\ x < 0\n\n\npost = 0 <= -x\n\n",
186+
"Type variables: <none>\n\n------------------------------------------------------------------------\nContext : hr: {x, y : int}\n\npre = p tt /\\ ! x < 0\n\n(1) y <- x \n\npost = 0 <= y\n\n"
187187
],
188188
"message":""
189189
},
190190
{
191191
"goals":[
192192
"Type variables: <none>\n\n------------------------------------------------------------------------\nforall &hr, p tt /\\ x{hr} < 0 => 0 <= -x{hr}\n",
193-
"Type variables: <none>\n\n------------------------------------------------------------------------\nContext : hr: {x, y : int}\n\npre = p tt /\\ ! x < 0\n\n(1) y <- x \n\npost = 0 <= y\n"
193+
"Type variables: <none>\n\n------------------------------------------------------------------------\nContext : hr: {x, y : int}\n\npre = p tt /\\ ! x < 0\n\n(1) y <- x \n\npost = 0 <= y\n\n"
194194
],
195195
"message":""
196196
},
197197
{
198198
"goals":[
199-
"Type variables: <none>\n\n------------------------------------------------------------------------\nContext : hr: {x, y : int}\n\npre = p tt /\\ ! x < 0\n\n(1) y <- x \n\npost = 0 <= y\n"
199+
"Type variables: <none>\n\n------------------------------------------------------------------------\nContext : hr: {x, y : int}\n\npre = p tt /\\ ! x < 0\n\n(1) y <- x \n\npost = 0 <= y\n\n"
200200
],
201201
"message":""
202202
},
203203
{
204204
"goals":[
205-
"Type variables: <none>\n\n------------------------------------------------------------------------\nContext : hr: {x, y : int}\n\npre = p tt /\\ ! x < 0\n\n\npost = 0 <= x\n"
205+
"Type variables: <none>\n\n------------------------------------------------------------------------\nContext : hr: {x, y : int}\n\npre = p tt /\\ ! x < 0\n\n\npost = 0 <= x\n\n"
206206
],
207207
"message":""
208208
},

0 commit comments

Comments
 (0)