forked from sven--/Software-Foundations
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Hoare2.html
2228 lines (1765 loc) · 239 KB
/
Hoare2.html
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
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8"/>
<link href="coqdoc.css" rel="stylesheet" type="text/css"/>
<title>Hoare2: Hoare Logic, Part II</title>
<script type="text/javascript" src="jquery-1.8.3.js"></script>
<script type="text/javascript" src="main.js"></script>
</head>
<body>
<div id="page">
<div id="header">
</div>
<div id="main">
<h1 class="libtitle">Hoare2<span class="subtitle">Hoare Logic, Part II</span></h1>
<div class="code code-tight">
</div>
<div class="doc">
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Require</span> <span class="id" type="keyword">Export</span> <span class="id" type="var">Hoare</span>.<br/>
<br/>
</div>
<div class="doc">
<a name="lab547"></a><h1 class="section">Decorated Programs</h1>
<div class="paragraph"> </div>
The beauty of Hoare Logic is that it is <i>compositional</i> —
the structure of proofs exactly follows the structure of programs.
This suggests that we can record the essential ideas of a proof
informally (leaving out some low-level calculational details) by
decorating programs with appropriate assertions around each
statement. Such a <i>decorated program</i> carries with it
an (informal) proof of its own correctness.
<div class="paragraph"> </div>
For example, here is a complete decorated program:
<div class="paragraph"> </div>
<div class="paragraph"> </div>
<div class="code code-tight">
<span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">True</span> <span style="letter-spacing:-.4em;">}</span>} <span style="font-family: arial;">⇾</span><br/>
<span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">m</span> = <span class="id" type="var">m</span> <span style="letter-spacing:-.4em;">}</span>}<br/>
<span class="id" type="var">X</span> ::= <span class="id" type="var">m</span>;<br/>
<span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">X</span> = <span class="id" type="var">m</span> <span style="letter-spacing:-.4em;">}</span>} <span style="font-family: arial;">⇾</span><br/>
<span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">X</span> = <span class="id" type="var">m</span> <span style="font-family: arial;">∧</span> <span class="id" type="var">p</span> = <span class="id" type="var">p</span> <span style="letter-spacing:-.4em;">}</span>}<br/>
<span class="id" type="var">Z</span> ::= <span class="id" type="var">p</span>;<br/>
<span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">X</span> = <span class="id" type="var">m</span> <span style="font-family: arial;">∧</span> <span class="id" type="var">Z</span> = <span class="id" type="var">p</span> <span style="letter-spacing:-.4em;">}</span>} <span style="font-family: arial;">⇾</span><br/>
<span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">Z</span> - <span class="id" type="var">X</span> = <span class="id" type="var">p</span> - <span class="id" type="var">m</span> <span style="letter-spacing:-.4em;">}</span>}<br/>
<span class="id" type="var">WHILE</span> <span class="id" type="var">X</span> ≠ 0 <span class="id" type="var">DO</span><br/>
<span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">Z</span> - <span class="id" type="var">X</span> = <span class="id" type="var">p</span> - <span class="id" type="var">m</span> <span style="font-family: arial;">∧</span> <span class="id" type="var">X</span> ≠ 0 <span style="letter-spacing:-.4em;">}</span>} <span style="font-family: arial;">⇾</span><br/>
<span style="letter-spacing:-.4em;">{</span>{ (<span class="id" type="var">Z</span> - 1) - (<span class="id" type="var">X</span> - 1) = <span class="id" type="var">p</span> - <span class="id" type="var">m</span> <span style="letter-spacing:-.4em;">}</span>}<br/>
<span class="id" type="var">Z</span> ::= <span class="id" type="var">Z</span> - 1;<br/>
<span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">Z</span> - (<span class="id" type="var">X</span> - 1) = <span class="id" type="var">p</span> - <span class="id" type="var">m</span> <span style="letter-spacing:-.4em;">}</span>}<br/>
<span class="id" type="var">X</span> ::= <span class="id" type="var">X</span> - 1<br/>
<span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">Z</span> - <span class="id" type="var">X</span> = <span class="id" type="var">p</span> - <span class="id" type="var">m</span> <span style="letter-spacing:-.4em;">}</span>}<br/>
<span class="id" type="var">END</span>;<br/>
<span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">Z</span> - <span class="id" type="var">X</span> = <span class="id" type="var">p</span> - <span class="id" type="var">m</span> <span style="font-family: arial;">∧</span> ¬ (<span class="id" type="var">X</span> ≠ 0) <span style="letter-spacing:-.4em;">}</span>} <span style="font-family: arial;">⇾</span><br/>
<span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">Z</span> = <span class="id" type="var">p</span> - <span class="id" type="var">m</span> <span style="letter-spacing:-.4em;">}</span>}
<div class="paragraph"> </div>
</div>
<div class="paragraph"> </div>
Concretely, a decorated program consists of the program text
interleaved with assertions. To check that a decorated program
represents a valid proof, we check that each individual command is
<i>locally consistent</i> with its accompanying assertions in the
following sense:
<div class="paragraph"> </div>
<div class="paragraph"> </div>
<ul class="doclist">
<li> <span class="inlinecode"><span class="id" type="var">SKIP</span></span> is locally consistent if its precondition and
postcondition are the same:
<div class="paragraph"> </div>
<div class="code code-tight">
<span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">P</span> <span style="letter-spacing:-.4em;">}</span>}<br/>
<span class="id" type="var">SKIP</span><br/>
<span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">P</span> <span style="letter-spacing:-.4em;">}</span>}
<div class="paragraph"> </div>
</div>
</li>
</ul>
<div class="paragraph"> </div>
<div class="paragraph"> </div>
<ul class="doclist">
<li> The sequential composition of <span class="inlinecode"><span class="id" type="var">c1</span></span> and <span class="inlinecode"><span class="id" type="var">c2</span></span> is locally
consistent (with respect to assertions <span class="inlinecode"><span class="id" type="var">P</span></span> and <span class="inlinecode"><span class="id" type="var">R</span></span>) if <span class="inlinecode"><span class="id" type="var">c1</span></span> is
locally consistent (with respect to <span class="inlinecode"><span class="id" type="var">P</span></span> and <span class="inlinecode"><span class="id" type="var">Q</span></span>) and <span class="inlinecode"><span class="id" type="var">c2</span></span> is
locally consistent (with respect to <span class="inlinecode"><span class="id" type="var">Q</span></span> and <span class="inlinecode"><span class="id" type="var">R</span></span>):
<div class="paragraph"> </div>
<div class="code code-tight">
<span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">P</span> <span style="letter-spacing:-.4em;">}</span>}<br/>
<span class="id" type="var">c1</span>;<br/>
<span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">Q</span> <span style="letter-spacing:-.4em;">}</span>}<br/>
<span class="id" type="var">c2</span><br/>
<span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">R</span> <span style="letter-spacing:-.4em;">}</span>}
<div class="paragraph"> </div>
</div>
</li>
</ul>
<div class="paragraph"> </div>
<div class="paragraph"> </div>
<ul class="doclist">
<li> An assignment is locally consistent if its precondition is
the appropriate substitution of its postcondition:
<div class="paragraph"> </div>
<div class="code code-tight">
<span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">P</span> [<span class="id" type="var">X</span> <span style="font-family: arial;">↦</span> <span class="id" type="var">a</span>] <span style="letter-spacing:-.4em;">}</span>}<br/>
<span class="id" type="var">X</span> ::= <span class="id" type="var">a</span><br/>
<span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">P</span> <span style="letter-spacing:-.4em;">}</span>}
<div class="paragraph"> </div>
</div>
</li>
</ul>
<div class="paragraph"> </div>
<div class="paragraph"> </div>
<ul class="doclist">
<li> A conditional is locally consistent (with respect to assertions
<span class="inlinecode"><span class="id" type="var">P</span></span> and <span class="inlinecode"><span class="id" type="var">Q</span></span>) if the assertions at the top of its "then" and
"else" branches are exactly <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode"><span style="font-family: arial;">∧</span></span> <span class="inlinecode"><span class="id" type="var">b</span></span> and <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode"><span style="font-family: arial;">∧</span></span> <span class="inlinecode">¬<span class="id" type="var">b</span></span> and if its "then"
branch is locally consistent (with respect to <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode"><span style="font-family: arial;">∧</span></span> <span class="inlinecode"><span class="id" type="var">b</span></span> and <span class="inlinecode"><span class="id" type="var">Q</span></span>)
and its "else" branch is locally consistent (with respect to
<span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode"><span style="font-family: arial;">∧</span></span> <span class="inlinecode">¬<span class="id" type="var">b</span></span> and <span class="inlinecode"><span class="id" type="var">Q</span></span>):
<div class="paragraph"> </div>
<div class="code code-tight">
<span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">P</span> <span style="letter-spacing:-.4em;">}</span>}<br/>
<span class="id" type="var">IFB</span> <span class="id" type="var">b</span> <span class="id" type="var">THEN</span><br/>
<span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">P</span> <span style="font-family: arial;">∧</span> <span class="id" type="var">b</span> <span style="letter-spacing:-.4em;">}</span>}<br/>
<span class="id" type="var">c1</span><br/>
<span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">Q</span> <span style="letter-spacing:-.4em;">}</span>}<br/>
<span class="id" type="var">ELSE</span><br/>
<span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">P</span> <span style="font-family: arial;">∧</span> ¬<span class="id" type="var">b</span> <span style="letter-spacing:-.4em;">}</span>}<br/>
<span class="id" type="var">c2</span><br/>
<span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">Q</span> <span style="letter-spacing:-.4em;">}</span>}<br/>
<span class="id" type="var">FI</span><br/>
<span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">Q</span> <span style="letter-spacing:-.4em;">}</span>}
<div class="paragraph"> </div>
</div>
</li>
</ul>
<div class="paragraph"> </div>
<div class="paragraph"> </div>
<ul class="doclist">
<li> A while loop with precondition <span class="inlinecode"><span class="id" type="var">P</span></span> is locally consistent if its
postcondition is <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode"><span style="font-family: arial;">∧</span></span> <span class="inlinecode">¬<span class="id" type="var">b</span></span> and if the pre- and postconditions of
its body are exactly <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode"><span style="font-family: arial;">∧</span></span> <span class="inlinecode"><span class="id" type="var">b</span></span> and <span class="inlinecode"><span class="id" type="var">P</span></span>:
<div class="paragraph"> </div>
<div class="code code-tight">
<span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">P</span> <span style="letter-spacing:-.4em;">}</span>}<br/>
<span class="id" type="var">WHILE</span> <span class="id" type="var">b</span> <span class="id" type="var">DO</span><br/>
<span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">P</span> <span style="font-family: arial;">∧</span> <span class="id" type="var">b</span> <span style="letter-spacing:-.4em;">}</span>}<br/>
<span class="id" type="var">c1</span><br/>
<span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">P</span> <span style="letter-spacing:-.4em;">}</span>}<br/>
<span class="id" type="var">END</span><br/>
<span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">P</span> <span style="font-family: arial;">∧</span> ¬<span class="id" type="var">b</span> <span style="letter-spacing:-.4em;">}</span>}
<div class="paragraph"> </div>
</div>
</li>
</ul>
<div class="paragraph"> </div>
<div class="paragraph"> </div>
<ul class="doclist">
<li> A pair of assertions separated by <span class="inlinecode"><span style="font-family: arial;">⇾</span></span> is locally consistent if
the first implies the second (in all states):
<div class="paragraph"> </div>
<div class="code code-tight">
<span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">P</span> <span style="letter-spacing:-.4em;">}</span>} <span style="font-family: arial;">⇾</span><br/>
<span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">P'</span> <span style="letter-spacing:-.4em;">}</span>}
<div class="paragraph"> </div>
</div>
<div class="paragraph"> </div>
This corresponds to the application of <span class="inlinecode"><span class="id" type="var">hoare_consequence</span></span> and
is the only place in a decorated program where checking if
decorations are correct is not fully mechanical and syntactic,
but involves logical and/or arithmetic reasoning.
</li>
</ul>
<div class="paragraph"> </div>
We have seen above how <i>verifying</i> the correctness of a
given proof involves checking that every single command is locally
consistent with the accompanying assertions. If we are instead
interested in <i>finding</i> a proof for a given specification we need
to discover the right assertions. This can be done in an almost
automatic way, with the exception of finding loop invariants,
which is the subject of in the next section. In the reminder of
this section we explain in detail how to construct decorations for
several simple programs that don't involve non-trivial loop
invariants.
</div>
<div class="code code-tight">
<br/>
</div>
<div class="doc">
<a name="lab548"></a><h2 class="section">Example: Swapping Using Addition and Subtraction</h2>
<div class="paragraph"> </div>
Here is a program that swaps the values of two variables using
addition and subtraction (instead of by assigning to a temporary
variable).
<div class="paragraph"> </div>
<div class="code code-tight">
<span class="id" type="var">X</span> ::= <span class="id" type="var">X</span> + <span class="id" type="var">Y</span>;<br/>
<span class="id" type="var">Y</span> ::= <span class="id" type="var">X</span> - <span class="id" type="var">Y</span>;<br/>
<span class="id" type="var">X</span> ::= <span class="id" type="var">X</span> - <span class="id" type="var">Y</span>
<div class="paragraph"> </div>
</div>
We can prove using decorations that this program is correct —
i.e., it always swaps the values of variables <span class="inlinecode"><span class="id" type="var">X</span></span> and <span class="inlinecode"><span class="id" type="var">Y</span></span>.
<div class="paragraph"> </div>
<div class="paragraph"> </div>
<div class="paragraph"> </div>
<div class="code code-tight">
(1) <span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">X</span> = <span class="id" type="var">m</span> <span style="font-family: arial;">∧</span> <span class="id" type="var">Y</span> = <span class="id" type="var">n</span> <span style="letter-spacing:-.4em;">}</span>} <span style="font-family: arial;">⇾</span><br/>
(2) <span style="letter-spacing:-.4em;">{</span>{ (<span class="id" type="var">X</span> + <span class="id" type="var">Y</span>) - ((<span class="id" type="var">X</span> + <span class="id" type="var">Y</span>) - <span class="id" type="var">Y</span>) = <span class="id" type="var">n</span> <span style="font-family: arial;">∧</span> (<span class="id" type="var">X</span> + <span class="id" type="var">Y</span>) - <span class="id" type="var">Y</span> = <span class="id" type="var">m</span> <span style="letter-spacing:-.4em;">}</span>}<br/>
<span class="id" type="var">X</span> ::= <span class="id" type="var">X</span> + <span class="id" type="var">Y</span>;<br/>
(3) <span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">X</span> - (<span class="id" type="var">X</span> - <span class="id" type="var">Y</span>) = <span class="id" type="var">n</span> <span style="font-family: arial;">∧</span> <span class="id" type="var">X</span> - <span class="id" type="var">Y</span> = <span class="id" type="var">m</span> <span style="letter-spacing:-.4em;">}</span>}<br/>
<span class="id" type="var">Y</span> ::= <span class="id" type="var">X</span> - <span class="id" type="var">Y</span>;<br/>
(4) <span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">X</span> - <span class="id" type="var">Y</span> = <span class="id" type="var">n</span> <span style="font-family: arial;">∧</span> <span class="id" type="var">Y</span> = <span class="id" type="var">m</span> <span style="letter-spacing:-.4em;">}</span>}<br/>
<span class="id" type="var">X</span> ::= <span class="id" type="var">X</span> - <span class="id" type="var">Y</span><br/>
(5) <span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">X</span> = <span class="id" type="var">n</span> <span style="font-family: arial;">∧</span> <span class="id" type="var">Y</span> = <span class="id" type="var">m</span> <span style="letter-spacing:-.4em;">}</span>}
<div class="paragraph"> </div>
</div>
The decorations were constructed as follows:
<div class="paragraph"> </div>
<ul class="doclist">
<li> We begin with the undecorated program (the unnumbered lines).
</li>
<li> We then add the specification — i.e., the outer
precondition (1) and postcondition (5). In the precondition we
use auxiliary variables (parameters) <span class="inlinecode"><span class="id" type="var">m</span></span> and <span class="inlinecode"><span class="id" type="var">n</span></span> to remember
the initial values of variables <span class="inlinecode"><span class="id" type="var">X</span></span> and respectively <span class="inlinecode"><span class="id" type="var">Y</span></span>, so
that we can refer to them in the postcondition (5).
</li>
<li> We work backwards mechanically starting from (5) all the way
to (2). At each step, we obtain the precondition of the
assignment from its postcondition by substituting the assigned
variable with the right-hand-side of the assignment. For
instance, we obtain (4) by substituting <span class="inlinecode"><span class="id" type="var">X</span></span> with <span class="inlinecode"><span class="id" type="var">X</span></span> <span class="inlinecode">-</span> <span class="inlinecode"><span class="id" type="var">Y</span></span>
in (5), and (3) by substituting <span class="inlinecode"><span class="id" type="var">Y</span></span> with <span class="inlinecode"><span class="id" type="var">X</span></span> <span class="inlinecode">-</span> <span class="inlinecode"><span class="id" type="var">Y</span></span> in (4).
</li>
<li> Finally, we verify that (1) logically implies (2) — i.e.,
that the step from (1) to (2) is a valid use of the law of
consequence. For this we substitute <span class="inlinecode"><span class="id" type="var">X</span></span> by <span class="inlinecode"><span class="id" type="var">m</span></span> and <span class="inlinecode"><span class="id" type="var">Y</span></span> by <span class="inlinecode"><span class="id" type="var">n</span></span>
and calculate as follows:
<div class="paragraph"> </div>
<div class="code code-tight">
(<span class="id" type="var">m</span> + <span class="id" type="var">n</span>) - ((<span class="id" type="var">m</span> + <span class="id" type="var">n</span>) - <span class="id" type="var">n</span>) = <span class="id" type="var">n</span> <span style="font-family: arial;">∧</span> (<span class="id" type="var">m</span> + <span class="id" type="var">n</span>) - <span class="id" type="var">n</span> = <span class="id" type="var">m</span><br/>
(<span class="id" type="var">m</span> + <span class="id" type="var">n</span>) - <span class="id" type="var">m</span> = <span class="id" type="var">n</span> <span style="font-family: arial;">∧</span> <span class="id" type="var">m</span> = <span class="id" type="var">m</span><br/>
<span class="id" type="var">n</span> = <span class="id" type="var">n</span> <span style="font-family: arial;">∧</span> <span class="id" type="var">m</span> = <span class="id" type="var">m</span>
<div class="paragraph"> </div>
</div>
</li>
</ul>
<div class="paragraph"> </div>
(Note that, since we are working with natural numbers, not
fixed-size machine integers, we don't need to worry about the
possibility of arithmetic overflow anywhere in this argument.)
</div>
<div class="code code-tight">
<br/>
</div>
<div class="doc">
<a name="lab549"></a><h2 class="section">Example: Simple Conditionals</h2>
<div class="paragraph"> </div>
Here is a simple decorated program using conditionals:
<div class="paragraph"> </div>
<div class="code code-tight">
(1) <span style="letter-spacing:-.4em;">{</span>{<span class="id" type="var">True</span><span style="letter-spacing:-.4em;">}</span>}<br/>
<span class="id" type="var">IFB</span> <span class="id" type="var">X</span> ≤ <span class="id" type="var">Y</span> <span class="id" type="var">THEN</span><br/>
(2) <span style="letter-spacing:-.4em;">{</span>{<span class="id" type="var">True</span> <span style="font-family: arial;">∧</span> <span class="id" type="var">X</span> ≤ <span class="id" type="var">Y</span><span style="letter-spacing:-.4em;">}</span>} <span style="font-family: arial;">⇾</span><br/>
(3) <span style="letter-spacing:-.4em;">{</span>{(<span class="id" type="var">Y</span> - <span class="id" type="var">X</span>) + <span class="id" type="var">X</span> = <span class="id" type="var">Y</span> <span style="font-family: arial;">∨</span> (<span class="id" type="var">Y</span> - <span class="id" type="var">X</span>) + <span class="id" type="var">Y</span> = <span class="id" type="var">X</span><span style="letter-spacing:-.4em;">}</span>}<br/>
<span class="id" type="var">Z</span> ::= <span class="id" type="var">Y</span> - <span class="id" type="var">X</span><br/>
(4) <span style="letter-spacing:-.4em;">{</span>{<span class="id" type="var">Z</span> + <span class="id" type="var">X</span> = <span class="id" type="var">Y</span> <span style="font-family: arial;">∨</span> <span class="id" type="var">Z</span> + <span class="id" type="var">Y</span> = <span class="id" type="var">X</span><span style="letter-spacing:-.4em;">}</span>}<br/>
<span class="id" type="var">ELSE</span><br/>
(5) <span style="letter-spacing:-.4em;">{</span>{<span class="id" type="var">True</span> <span style="font-family: arial;">∧</span> ~(<span class="id" type="var">X</span> ≤ <span class="id" type="var">Y</span>) <span style="letter-spacing:-.4em;">}</span>} <span style="font-family: arial;">⇾</span><br/>
(6) <span style="letter-spacing:-.4em;">{</span>{(<span class="id" type="var">X</span> - <span class="id" type="var">Y</span>) + <span class="id" type="var">X</span> = <span class="id" type="var">Y</span> <span style="font-family: arial;">∨</span> (<span class="id" type="var">X</span> - <span class="id" type="var">Y</span>) + <span class="id" type="var">Y</span> = <span class="id" type="var">X</span><span style="letter-spacing:-.4em;">}</span>}<br/>
<span class="id" type="var">Z</span> ::= <span class="id" type="var">X</span> - <span class="id" type="var">Y</span><br/>
(7) <span style="letter-spacing:-.4em;">{</span>{<span class="id" type="var">Z</span> + <span class="id" type="var">X</span> = <span class="id" type="var">Y</span> <span style="font-family: arial;">∨</span> <span class="id" type="var">Z</span> + <span class="id" type="var">Y</span> = <span class="id" type="var">X</span><span style="letter-spacing:-.4em;">}</span>}<br/>
<span class="id" type="var">FI</span><br/>
(8) <span style="letter-spacing:-.4em;">{</span>{<span class="id" type="var">Z</span> + <span class="id" type="var">X</span> = <span class="id" type="var">Y</span> <span style="font-family: arial;">∨</span> <span class="id" type="var">Z</span> + <span class="id" type="var">Y</span> = <span class="id" type="var">X</span><span style="letter-spacing:-.4em;">}</span>}
<div class="paragraph"> </div>
</div>
<div class="paragraph"> </div>
These decorations were constructed as follows:
<div class="paragraph"> </div>
<ul class="doclist">
<li> We start with the outer precondition (1) and postcondition (8).
</li>
<li> We follow the format dictated by the <span class="inlinecode"><span class="id" type="var">hoare_if</span></span> rule and copy the
postcondition (8) to (4) and (7). We conjoin the precondition (1)
with the guard of the conditional to obtain (2). We conjoin (1)
with the negated guard of the conditional to obtain (5).
</li>
<li> In order to use the assignment rule and obtain (3), we substitute
<span class="inlinecode"><span class="id" type="var">Z</span></span> by <span class="inlinecode"><span class="id" type="var">Y</span></span> <span class="inlinecode">-</span> <span class="inlinecode"><span class="id" type="var">X</span></span> in (4). To obtain (6) we substitute <span class="inlinecode"><span class="id" type="var">Z</span></span> by <span class="inlinecode"><span class="id" type="var">X</span></span> <span class="inlinecode">-</span> <span class="inlinecode"><span class="id" type="var">Y</span></span>
in (7).
</li>
<li> Finally, we verify that (2) implies (3) and (5) implies (6). Both
of these implications crucially depend on the ordering of <span class="inlinecode"><span class="id" type="var">X</span></span> and
<span class="inlinecode"><span class="id" type="var">Y</span></span> obtained from the guard. For instance, knowing that <span class="inlinecode"><span class="id" type="var">X</span></span> <span class="inlinecode">≤</span> <span class="inlinecode"><span class="id" type="var">Y</span></span>
ensures that subtracting <span class="inlinecode"><span class="id" type="var">X</span></span> from <span class="inlinecode"><span class="id" type="var">Y</span></span> and then adding back <span class="inlinecode"><span class="id" type="var">X</span></span>
produces <span class="inlinecode"><span class="id" type="var">Y</span></span>, as required by the first disjunct of (3). Similarly,
knowing that <span class="inlinecode">~(<span class="id" type="var">X</span></span> <span class="inlinecode">≤</span> <span class="inlinecode"><span class="id" type="var">Y</span>)</span> ensures that subtracting <span class="inlinecode"><span class="id" type="var">Y</span></span> from <span class="inlinecode"><span class="id" type="var">X</span></span> and
then adding back <span class="inlinecode"><span class="id" type="var">Y</span></span> produces <span class="inlinecode"><span class="id" type="var">X</span></span>, as needed by the second
disjunct of (6). Note that <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">-</span> <span class="inlinecode"><span class="id" type="var">m</span></span> <span class="inlinecode">+</span> <span class="inlinecode"><span class="id" type="var">m</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">n</span></span> does <i>not</i> hold for
arbitrary natural numbers <span class="inlinecode"><span class="id" type="var">n</span></span> and <span class="inlinecode"><span class="id" type="var">m</span></span> (for example, <span class="inlinecode">3</span> <span class="inlinecode">-</span> <span class="inlinecode">5</span> <span class="inlinecode">+</span> <span class="inlinecode">5</span> <span class="inlinecode">=</span>
<span class="inlinecode">5</span>).
</li>
</ul>
<div class="paragraph"> </div>
<a name="lab550"></a><h4 class="section">Exercise: 2 stars (if_minus_plus_reloaded)</h4>
Fill in valid decorations for the following program:
<div class="paragraph"> </div>
<div class="code code-tight">
<span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">True</span> <span style="letter-spacing:-.4em;">}</span>}<br/>
<span class="id" type="var">IFB</span> <span class="id" type="var">X</span> ≤ <span class="id" type="var">Y</span> <span class="id" type="var">THEN</span><br/>
<span style="letter-spacing:-.4em;">{</span>{ <span style="letter-spacing:-.4em;">}</span>} <span style="font-family: arial;">⇾</span><br/>
<span style="letter-spacing:-.4em;">{</span>{ <span style="letter-spacing:-.4em;">}</span>}<br/>
<span class="id" type="var">Z</span> ::= <span class="id" type="var">Y</span> - <span class="id" type="var">X</span><br/>
<span style="letter-spacing:-.4em;">{</span>{ <span style="letter-spacing:-.4em;">}</span>}<br/>
<span class="id" type="var">ELSE</span><br/>
<span style="letter-spacing:-.4em;">{</span>{ <span style="letter-spacing:-.4em;">}</span>} <span style="font-family: arial;">⇾</span><br/>
<span style="letter-spacing:-.4em;">{</span>{ <span style="letter-spacing:-.4em;">}</span>}<br/>
<span class="id" type="var">Y</span> ::= <span class="id" type="var">X</span> + <span class="id" type="var">Z</span><br/>
<span style="letter-spacing:-.4em;">{</span>{ <span style="letter-spacing:-.4em;">}</span>}<br/>
<span class="id" type="var">FI</span><br/>
<span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">Y</span> = <span class="id" type="var">X</span> + <span class="id" type="var">Z</span> <span style="letter-spacing:-.4em;">}</span>}
<div class="paragraph"> </div>
</div>
</div>
<div class="code code-tight">
<br/>
</div>
<div class="doc">
<a name="lab551"></a><h2 class="section">Example: Reduce to Zero (Trivial Loop)</h2>
<div class="paragraph"> </div>
Here is a <span class="inlinecode"><span class="id" type="var">WHILE</span></span> loop that is so simple it needs no
invariant (i.e., the invariant <span class="inlinecode"><span class="id" type="var">True</span></span> will do the job).
<div class="paragraph"> </div>
<div class="code code-tight">
(1) <span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">True</span> <span style="letter-spacing:-.4em;">}</span>}<br/>
<span class="id" type="var">WHILE</span> <span class="id" type="var">X</span> ≠ 0 <span class="id" type="var">DO</span><br/>
(2) <span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">True</span> <span style="font-family: arial;">∧</span> <span class="id" type="var">X</span> ≠ 0 <span style="letter-spacing:-.4em;">}</span>} <span style="font-family: arial;">⇾</span><br/>
(3) <span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">True</span> <span style="letter-spacing:-.4em;">}</span>}<br/>
<span class="id" type="var">X</span> ::= <span class="id" type="var">X</span> - 1<br/>
(4) <span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">True</span> <span style="letter-spacing:-.4em;">}</span>}<br/>
<span class="id" type="var">END</span><br/>
(5) <span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">True</span> <span style="font-family: arial;">∧</span> <span class="id" type="var">X</span> = 0 <span style="letter-spacing:-.4em;">}</span>} <span style="font-family: arial;">⇾</span><br/>
(6) <span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">X</span> = 0 <span style="letter-spacing:-.4em;">}</span>}
<div class="paragraph"> </div>
</div>
The decorations can be constructed as follows:
<div class="paragraph"> </div>
<ul class="doclist">
<li> Start with the outer precondition (1) and postcondition (6).
</li>
<li> Following the format dictated by the <span class="inlinecode"><span class="id" type="var">hoare_while</span></span> rule, we copy
(1) to (4). We conjoin (1) with the guard to obtain (2) and with
the negation of the guard to obtain (5). Note that, because the
outer postcondition (6) does not syntactically match (5), we need a
trivial use of the consequence rule from (5) to (6).
</li>
<li> Assertion (3) is the same as (4), because <span class="inlinecode"><span class="id" type="var">X</span></span> does not appear in
<span class="inlinecode">4</span>, so the substitution in the assignment rule is trivial.
</li>
<li> Finally, the implication between (2) and (3) is also trivial.
</li>
</ul>
<div class="paragraph"> </div>
From this informal proof, it is easy to read off a formal proof
using the Coq versions of the Hoare rules. Note that we do <i>not</i>
unfold the definition of <span class="inlinecode"><span class="id" type="var">hoare_triple</span></span> anywhere in this proof —
the idea is to use the Hoare rules as a "self-contained" logic for
reasoning about programs.
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">reduce_to_zero'</span> : <span class="id" type="var">com</span> :=<br/>
<span class="id" type="var">WHILE</span> <span class="id" type="var">BNot</span> (<span class="id" type="var">BEq</span> (<span class="id" type="var">AId</span> <span class="id" type="var">X</span>) (<span class="id" type="var">ANum</span> 0)) <span class="id" type="var">DO</span><br/>
<span class="id" type="var">X</span> ::= <span class="id" type="var">AMinus</span> (<span class="id" type="var">AId</span> <span class="id" type="var">X</span>) (<span class="id" type="var">ANum</span> 1)<br/>
<span class="id" type="var">END</span>.<br/>
<br/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">reduce_to_zero_correct'</span> :<br/>
<span style="letter-spacing:-.4em;">{</span>{<span class="id" type="keyword">fun</span> <span class="id" type="var">st</span> ⇒ <span class="id" type="var">True</span><span style="letter-spacing:-.4em;">}</span>}<br/>
<span class="id" type="var">reduce_to_zero'</span><br/>
<span style="letter-spacing:-.4em;">{</span>{<span class="id" type="keyword">fun</span> <span class="id" type="var">st</span> ⇒ <span class="id" type="var">st</span> <span class="id" type="var">X</span> = 0<span style="letter-spacing:-.4em;">}</span>}.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="id" type="tactic">unfold</span> <span class="id" type="var">reduce_to_zero'</span>.<br/>
<span class="comment">(* First we need to transform the postcondition so<br/>
that hoare_while will apply. *)</span><br/>
<span class="id" type="tactic">eapply</span> <span class="id" type="var">hoare_consequence_post</span>.<br/>
<span class="id" type="tactic">apply</span> <span class="id" type="var">hoare_while</span>.<br/>
<span class="id" type="var">Case</span> "Loop body preserves invariant".<br/>
<span class="comment">(* Need to massage precondition before <span class="inlinecode"><span class="id" type="var">hoare_asgn</span></span> applies *)</span><br/>
<span class="id" type="tactic">eapply</span> <span class="id" type="var">hoare_consequence_pre</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">hoare_asgn</span>.<br/>
<span class="comment">(* Proving trivial implication (2) ->> (3) *)</span><br/>
<span class="id" type="tactic">intros</span> <span class="id" type="var">st</span> [<span class="id" type="var">HT</span> <span class="id" type="var">Hbp</span>]. <span class="id" type="tactic">unfold</span> <span class="id" type="var">assn_sub</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">I</span>.<br/>
<span class="id" type="var">Case</span> "Invariant and negated guard imply postcondition".<br/>
<span class="id" type="tactic">intros</span> <span class="id" type="var">st</span> [<span class="id" type="var">Inv</span> <span class="id" type="var">GuardFalse</span>].<br/>
<span class="id" type="tactic">unfold</span> <span class="id" type="var">bassn</span> <span class="id" type="keyword">in</span> <span class="id" type="var">GuardFalse</span>. <span class="id" type="tactic">simpl</span> <span class="id" type="keyword">in</span> <span class="id" type="var">GuardFalse</span>.<br/>
<span class="comment">(* SearchAbout helps to find the right lemmas *)</span><br/>
<span class="id" type="var">Search</span><span class="id" type="var">About</span> [<span class="id" type="var">not</span> <span class="id" type="var">true</span>].<br/>
<span class="id" type="tactic">rewrite</span> <span class="id" type="var">not_true_iff_false</span> <span class="id" type="keyword">in</span> <span class="id" type="var">GuardFalse</span>.<br/>
<span class="id" type="var">Search</span><span class="id" type="var">About</span> [<span class="id" type="var">negb</span> <span class="id" type="var">false</span>].<br/>
<span class="id" type="tactic">rewrite</span> <span class="id" type="var">negb_false_iff</span> <span class="id" type="keyword">in</span> <span class="id" type="var">GuardFalse</span>.<br/>
<span class="id" type="var">Search</span><span class="id" type="var">About</span> [<span class="id" type="var">beq_nat</span> <span class="id" type="var">true</span>].<br/>
<span class="id" type="tactic">apply</span> <span class="id" type="var">beq_nat_true</span> <span class="id" type="keyword">in</span> <span class="id" type="var">GuardFalse</span>.<br/>
<span class="id" type="tactic">apply</span> <span class="id" type="var">GuardFalse</span>. <span class="id" type="keyword">Qed</span>.<br/>
<br/>
</div>
<div class="doc">
<a name="lab552"></a><h2 class="section">Example: Division</h2>
<div class="paragraph"> </div>
The following Imp program calculates the integer division and
remainder of two numbers <span class="inlinecode"><span class="id" type="var">m</span></span> and <span class="inlinecode"><span class="id" type="var">n</span></span> that are arbitrary constants
in the program.
<div class="paragraph"> </div>
<div class="code code-tight">
<span class="id" type="var">X</span> ::= <span class="id" type="var">m</span>;<br/>
<span class="id" type="var">Y</span> ::= 0;<br/>
<span class="id" type="var">WHILE</span> <span class="id" type="var">n</span> ≤ <span class="id" type="var">X</span> <span class="id" type="var">DO</span><br/>
<span class="id" type="var">X</span> ::= <span class="id" type="var">X</span> - <span class="id" type="var">n</span>;<br/>
<span class="id" type="var">Y</span> ::= <span class="id" type="var">Y</span> + 1<br/>
<span class="id" type="var">END</span>;
<div class="paragraph"> </div>
</div>
In other words, if we replace <span class="inlinecode"><span class="id" type="var">m</span></span> and <span class="inlinecode"><span class="id" type="var">n</span></span> by concrete numbers and
execute the program, it will terminate with the variable <span class="inlinecode"><span class="id" type="var">X</span></span> set
to the remainder when <span class="inlinecode"><span class="id" type="var">m</span></span> is divided by <span class="inlinecode"><span class="id" type="var">n</span></span> and <span class="inlinecode"><span class="id" type="var">Y</span></span> set to the
quotient.
<div class="paragraph"> </div>
In order to give a specification to this program we need to
remember that dividing <span class="inlinecode"><span class="id" type="var">m</span></span> by <span class="inlinecode"><span class="id" type="var">n</span></span> produces a reminder <span class="inlinecode"><span class="id" type="var">X</span></span> and a
quotient <span class="inlinecode"><span class="id" type="var">Y</span></span> so that <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">×</span> <span class="inlinecode"><span class="id" type="var">Y</span></span> <span class="inlinecode">+</span> <span class="inlinecode"><span class="id" type="var">X</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">m</span></span> <span class="inlinecode"><span style="font-family: arial;">∧</span></span> <span class="inlinecode"><span class="id" type="var">X</span></span> <span class="inlinecode"><</span> <span class="inlinecode"><span class="id" type="var">n</span></span>.
<div class="paragraph"> </div>
It turns out that we get lucky with this program and don't have to
think very hard about the loop invariant: the invariant is the
just first conjunct <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">×</span> <span class="inlinecode"><span class="id" type="var">Y</span></span> <span class="inlinecode">+</span> <span class="inlinecode"><span class="id" type="var">X</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">m</span></span>, so we use that to decorate
the program.
<div class="paragraph"> </div>
<div class="paragraph"> </div>
<div class="code code-tight">
(1) <span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">True</span> <span style="letter-spacing:-.4em;">}</span>} <span style="font-family: arial;">⇾</span><br/>
(2) <span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">n</span> × 0 + <span class="id" type="var">m</span> = <span class="id" type="var">m</span> <span style="letter-spacing:-.4em;">}</span>}<br/>
<span class="id" type="var">X</span> ::= <span class="id" type="var">m</span>;<br/>
(3) <span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">n</span> × 0 + <span class="id" type="var">X</span> = <span class="id" type="var">m</span> <span style="letter-spacing:-.4em;">}</span>}<br/>
<span class="id" type="var">Y</span> ::= 0;<br/>
(4) <span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">n</span> × <span class="id" type="var">Y</span> + <span class="id" type="var">X</span> = <span class="id" type="var">m</span> <span style="letter-spacing:-.4em;">}</span>}<br/>
<span class="id" type="var">WHILE</span> <span class="id" type="var">n</span> ≤ <span class="id" type="var">X</span> <span class="id" type="var">DO</span><br/>
(5) <span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">n</span> × <span class="id" type="var">Y</span> + <span class="id" type="var">X</span> = <span class="id" type="var">m</span> <span style="font-family: arial;">∧</span> <span class="id" type="var">n</span> ≤ <span class="id" type="var">X</span> <span style="letter-spacing:-.4em;">}</span>} <span style="font-family: arial;">⇾</span><br/>
(6) <span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">n</span> × (<span class="id" type="var">Y</span> + 1) + (<span class="id" type="var">X</span> - <span class="id" type="var">n</span>) = <span class="id" type="var">m</span> <span style="letter-spacing:-.4em;">}</span>}<br/>
<span class="id" type="var">X</span> ::= <span class="id" type="var">X</span> - <span class="id" type="var">n</span>;<br/>
(7) <span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">n</span> × (<span class="id" type="var">Y</span> + 1) + <span class="id" type="var">X</span> = <span class="id" type="var">m</span> <span style="letter-spacing:-.4em;">}</span>}<br/>
<span class="id" type="var">Y</span> ::= <span class="id" type="var">Y</span> + 1<br/>
(8) <span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">n</span> × <span class="id" type="var">Y</span> + <span class="id" type="var">X</span> = <span class="id" type="var">m</span> <span style="letter-spacing:-.4em;">}</span>}<br/>
<span class="id" type="var">END</span><br/>
(9) <span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">n</span> × <span class="id" type="var">Y</span> + <span class="id" type="var">X</span> = <span class="id" type="var">m</span> <span style="font-family: arial;">∧</span> <span class="id" type="var">X</span> < <span class="id" type="var">n</span> <span style="letter-spacing:-.4em;">}</span>}
<div class="paragraph"> </div>
</div>
<div class="paragraph"> </div>
Assertions (4), (5), (8), and (9) are derived mechanically from
the invariant and the loop's guard. Assertions (8), (7), and (6)
are derived using the assignment rule going backwards from (8) to
(6). Assertions (4), (3), and (2) are again backwards applications
of the assignment rule.
<div class="paragraph"> </div>
Now that we've decorated the program it only remains to check that
the two uses of the consequence rule are correct — i.e., that (1)
implies (2) and that (5) implies (6). This is indeed the case, so
we have a valid decorated program.
</div>
<div class="code code-tight">
<br/>
</div>
<div class="doc">
<a name="lab553"></a><h1 class="section">Finding Loop Invariants</h1>
<div class="paragraph"> </div>
Once the outermost precondition and postcondition are chosen, the
only creative part in verifying programs with Hoare Logic is
finding the right loop invariants. The reason this is difficult
is the same as the reason that doing inductive mathematical proofs
requires creativity: strengthening the loop invariant (or the
induction hypothesis) means that you have a stronger assumption to
work with when trying to establish the postcondition of the loop
body (complete the induction step of the proof), but it also means
that the loop body postcondition itself is harder to prove!
<div class="paragraph"> </div>
This section is dedicated to teaching you how to approach the
challenge of finding loop invariants using a series of examples
and exercises.
<div class="paragraph"> </div>
<a name="lab554"></a><h2 class="section">Example: Slow Subtraction</h2>
<div class="paragraph"> </div>
The following program subtracts the value of <span class="inlinecode"><span class="id" type="var">X</span></span> from the value of
<span class="inlinecode"><span class="id" type="var">Y</span></span> by repeatedly decrementing both <span class="inlinecode"><span class="id" type="var">X</span></span> and <span class="inlinecode"><span class="id" type="var">Y</span></span>. We want to verify its
correctness with respect to the following specification:
<div class="paragraph"> </div>
<div class="code code-tight">
<span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">X</span> = <span class="id" type="var">m</span> <span style="font-family: arial;">∧</span> <span class="id" type="var">Y</span> = <span class="id" type="var">n</span> <span style="letter-spacing:-.4em;">}</span>}<br/>
<span class="id" type="var">WHILE</span> <span class="id" type="var">X</span> ≠ 0 <span class="id" type="var">DO</span><br/>
<span class="id" type="var">Y</span> ::= <span class="id" type="var">Y</span> - 1;<br/>
<span class="id" type="var">X</span> ::= <span class="id" type="var">X</span> - 1<br/>
<span class="id" type="var">END</span><br/>
<span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">Y</span> = <span class="id" type="var">n</span> - <span class="id" type="var">m</span> <span style="letter-spacing:-.4em;">}</span>}
<div class="paragraph"> </div>
</div>
<div class="paragraph"> </div>
To verify this program we need to find an invariant <span class="inlinecode"><span class="id" type="var">I</span></span> for the
loop. As a first step we can leave <span class="inlinecode"><span class="id" type="var">I</span></span> as an unknown and build a
<i>skeleton</i> for the proof by applying backward the rules for local
consistency. This process leads to the following skeleton:
<div class="paragraph"> </div>
<div class="code code-tight">
(1) <span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">X</span> = <span class="id" type="var">m</span> <span style="font-family: arial;">∧</span> <span class="id" type="var">Y</span> = <span class="id" type="var">n</span> <span style="letter-spacing:-.4em;">}</span>} <span style="font-family: arial;">⇾</span> (<span class="id" type="var">a</span>)<br/>
(2) <span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">I</span> <span style="letter-spacing:-.4em;">}</span>}<br/>
<span class="id" type="var">WHILE</span> <span class="id" type="var">X</span> ≠ 0 <span class="id" type="var">DO</span><br/>
(3) <span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">I</span> <span style="font-family: arial;">∧</span> <span class="id" type="var">X</span> ≠ 0 <span style="letter-spacing:-.4em;">}</span>} <span style="font-family: arial;">⇾</span> (<span class="id" type="var">c</span>)<br/>
(4) <span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">I</span>[<span class="id" type="var">X</span> <span style="font-family: arial;">↦</span> <span class="id" type="var">X</span>-1][<span class="id" type="var">Y</span> <span style="font-family: arial;">↦</span> <span class="id" type="var">Y</span>-1] <span style="letter-spacing:-.4em;">}</span>}<br/>
<span class="id" type="var">Y</span> ::= <span class="id" type="var">Y</span> - 1;<br/>
(5) <span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">I</span>[<span class="id" type="var">X</span> <span style="font-family: arial;">↦</span> <span class="id" type="var">X</span>-1] <span style="letter-spacing:-.4em;">}</span>}<br/>
<span class="id" type="var">X</span> ::= <span class="id" type="var">X</span> - 1<br/>
(6) <span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">I</span> <span style="letter-spacing:-.4em;">}</span>}<br/>
<span class="id" type="var">END</span><br/>
(7) <span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">I</span> <span style="font-family: arial;">∧</span> ~(<span class="id" type="var">X</span> ≠ 0) <span style="letter-spacing:-.4em;">}</span>} <span style="font-family: arial;">⇾</span> (<span class="id" type="var">b</span>)<br/>
(8) <span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">Y</span> = <span class="id" type="var">n</span> - <span class="id" type="var">m</span> <span style="letter-spacing:-.4em;">}</span>}
<div class="paragraph"> </div>
</div>
<div class="paragraph"> </div>
By examining this skeleton, we can see that any valid <span class="inlinecode"><span class="id" type="var">I</span></span> will
have to respect three conditions:
<div class="paragraph"> </div>
<ul class="doclist">
<li> (a) it must be weak enough to be implied by the loop's
precondition, i.e. (1) must imply (2);
</li>
<li> (b) it must be strong enough to imply the loop's postcondition,
i.e. (7) must imply (8);
</li>
<li> (c) it must be preserved by one iteration of the loop, i.e. (3)
must imply (4).
</li>
</ul>
<div class="paragraph"> </div>
These conditions are actually independent of the particular
program and specification we are considering. Indeed, every loop
invariant has to satisfy them. One way to find an invariant that
simultaneously satisfies these three conditions is by using an
iterative process: start with a "candidate" invariant (e.g. a
guess or a heuristic choice) and check the three conditions above;
if any of the checks fails, try to use the information that we get
from the failure to produce another (hopefully better) candidate
invariant, and repeat the process.
<div class="paragraph"> </div>
For instance, in the reduce-to-zero example above, we saw that,
for a very simple loop, choosing <span class="inlinecode"><span class="id" type="var">True</span></span> as an invariant did the
job. So let's try it again here! I.e., let's instantiate <span class="inlinecode"><span class="id" type="var">I</span></span> with
<span class="inlinecode"><span class="id" type="var">True</span></span> in the skeleton above see what we get...
<div class="paragraph"> </div>
<div class="code code-tight">
(1) <span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">X</span> = <span class="id" type="var">m</span> <span style="font-family: arial;">∧</span> <span class="id" type="var">Y</span> = <span class="id" type="var">n</span> <span style="letter-spacing:-.4em;">}</span>} <span style="font-family: arial;">⇾</span> (<span class="id" type="var">a</span> - <span class="id" type="var">OK</span>)<br/>
(2) <span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">True</span> <span style="letter-spacing:-.4em;">}</span>}<br/>
<span class="id" type="var">WHILE</span> <span class="id" type="var">X</span> ≠ 0 <span class="id" type="var">DO</span><br/>
(3) <span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">True</span> <span style="font-family: arial;">∧</span> <span class="id" type="var">X</span> ≠ 0 <span style="letter-spacing:-.4em;">}</span>} <span style="font-family: arial;">⇾</span> (<span class="id" type="var">c</span> - <span class="id" type="var">OK</span>)<br/>
(4) <span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">True</span> <span style="letter-spacing:-.4em;">}</span>}<br/>
<span class="id" type="var">Y</span> ::= <span class="id" type="var">Y</span> - 1;<br/>
(5) <span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">True</span> <span style="letter-spacing:-.4em;">}</span>}<br/>
<span class="id" type="var">X</span> ::= <span class="id" type="var">X</span> - 1<br/>
(6) <span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">True</span> <span style="letter-spacing:-.4em;">}</span>}<br/>
<span class="id" type="var">END</span><br/>
(7) <span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">True</span> <span style="font-family: arial;">∧</span> <span class="id" type="var">X</span> = 0 <span style="letter-spacing:-.4em;">}</span>} <span style="font-family: arial;">⇾</span> (<span class="id" type="var">b</span> - <span class="id" type="var">WRONG</span>!)<br/>
(8) <span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">Y</span> = <span class="id" type="var">n</span> - <span class="id" type="var">m</span> <span style="letter-spacing:-.4em;">}</span>}
<div class="paragraph"> </div>
</div>
<div class="paragraph"> </div>
While conditions (a) and (c) are trivially satisfied,
condition (b) is wrong, i.e. it is not the case that (7) <span class="inlinecode"><span class="id" type="var">True</span></span> <span class="inlinecode"><span style="font-family: arial;">∧</span></span>
<span class="inlinecode"><span class="id" type="var">X</span></span> <span class="inlinecode">=</span> <span class="inlinecode">0</span> implies (8) <span class="inlinecode"><span class="id" type="var">Y</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">-</span> <span class="inlinecode"><span class="id" type="var">m</span></span>. In fact, the two assertions are
completely unrelated and it is easy to find a counterexample (say,
<span class="inlinecode"><span class="id" type="var">Y</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">X</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">m</span></span> <span class="inlinecode">=</span> <span class="inlinecode">0</span> and <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode">1</span>).
<div class="paragraph"> </div>
If we want (b) to hold, we need to strengthen the invariant so
that it implies the postcondition (8). One very simple way to do
this is to let the invariant <i>be</i> the postcondition. So let's
return to our skeleton, instantiate <span class="inlinecode"><span class="id" type="var">I</span></span> with <span class="inlinecode"><span class="id" type="var">Y</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">-</span> <span class="inlinecode"><span class="id" type="var">m</span></span>, and
check conditions (a) to (c) again.
<div class="paragraph"> </div>
<div class="code code-tight">
(1) <span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">X</span> = <span class="id" type="var">m</span> <span style="font-family: arial;">∧</span> <span class="id" type="var">Y</span> = <span class="id" type="var">n</span> <span style="letter-spacing:-.4em;">}</span>} <span style="font-family: arial;">⇾</span> (<span class="id" type="var">a</span> - <span class="id" type="var">WRONG</span>!)<br/>
(2) <span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">Y</span> = <span class="id" type="var">n</span> - <span class="id" type="var">m</span> <span style="letter-spacing:-.4em;">}</span>}<br/>
<span class="id" type="var">WHILE</span> <span class="id" type="var">X</span> ≠ 0 <span class="id" type="var">DO</span><br/>
(3) <span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">Y</span> = <span class="id" type="var">n</span> - <span class="id" type="var">m</span> <span style="font-family: arial;">∧</span> <span class="id" type="var">X</span> ≠ 0 <span style="letter-spacing:-.4em;">}</span>} <span style="font-family: arial;">⇾</span> (<span class="id" type="var">c</span> - <span class="id" type="var">WRONG</span>!)<br/>
(4) <span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">Y</span> - 1 = <span class="id" type="var">n</span> - <span class="id" type="var">m</span> <span style="letter-spacing:-.4em;">}</span>}<br/>
<span class="id" type="var">Y</span> ::= <span class="id" type="var">Y</span> - 1;<br/>
(5) <span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">Y</span> = <span class="id" type="var">n</span> - <span class="id" type="var">m</span> <span style="letter-spacing:-.4em;">}</span>}<br/>
<span class="id" type="var">X</span> ::= <span class="id" type="var">X</span> - 1<br/>
(6) <span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">Y</span> = <span class="id" type="var">n</span> - <span class="id" type="var">m</span> <span style="letter-spacing:-.4em;">}</span>}<br/>
<span class="id" type="var">END</span><br/>
(7) <span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">Y</span> = <span class="id" type="var">n</span> - <span class="id" type="var">m</span> <span style="font-family: arial;">∧</span> <span class="id" type="var">X</span> = 0 <span style="letter-spacing:-.4em;">}</span>} <span style="font-family: arial;">⇾</span> (<span class="id" type="var">b</span> - <span class="id" type="var">OK</span>)<br/>
(8) <span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">Y</span> = <span class="id" type="var">n</span> - <span class="id" type="var">m</span> <span style="letter-spacing:-.4em;">}</span>}
<div class="paragraph"> </div>
</div>
<div class="paragraph"> </div>
This time, condition (b) holds trivially, but (a) and (c) are
broken. Condition (a) requires that (1) <span class="inlinecode"><span class="id" type="var">X</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">m</span></span> <span class="inlinecode"><span style="font-family: arial;">∧</span></span> <span class="inlinecode"><span class="id" type="var">Y</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">n</span></span>
implies (2) <span class="inlinecode"><span class="id" type="var">Y</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">-</span> <span class="inlinecode"><span class="id" type="var">m</span></span>. If we substitute <span class="inlinecode"><span class="id" type="var">Y</span></span> by <span class="inlinecode"><span class="id" type="var">n</span></span> we have to
show that <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">-</span> <span class="inlinecode"><span class="id" type="var">m</span></span> for arbitrary <span class="inlinecode"><span class="id" type="var">m</span></span> and <span class="inlinecode"><span class="id" type="var">n</span></span>, which does not
hold (for instance, when <span class="inlinecode"><span class="id" type="var">m</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode">1</span>). Condition (c) requires that
<span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">-</span> <span class="inlinecode"><span class="id" type="var">m</span></span> <span class="inlinecode">-</span> <span class="inlinecode">1</span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">-</span> <span class="inlinecode"><span class="id" type="var">m</span></span>, which fails, for instance, for <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode">1</span> and <span class="inlinecode"><span class="id" type="var">m</span></span> <span class="inlinecode">=</span>
<span class="inlinecode">0</span>. So, although <span class="inlinecode"><span class="id" type="var">Y</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">-</span> <span class="inlinecode"><span class="id" type="var">m</span></span> holds at the end of the loop, it does
not hold from the start, and it doesn't hold on each iteration;
it is not a correct invariant.
<div class="paragraph"> </div>
This failure is not very surprising: the variable <span class="inlinecode"><span class="id" type="var">Y</span></span> changes
during the loop, while <span class="inlinecode"><span class="id" type="var">m</span></span> and <span class="inlinecode"><span class="id" type="var">n</span></span> are constant, so the assertion
we chose didn't have much chance of being an invariant!
<div class="paragraph"> </div>
To do better, we need to generalize (8) to some statement that is
equivalent to (8) when <span class="inlinecode"><span class="id" type="var">X</span></span> is <span class="inlinecode">0</span>, since this will be the case
when the loop terminates, and that "fills the gap" in some
appropriate way when <span class="inlinecode"><span class="id" type="var">X</span></span> is nonzero. Looking at how the loop
works, we can observe that <span class="inlinecode"><span class="id" type="var">X</span></span> and <span class="inlinecode"><span class="id" type="var">Y</span></span> are decremented together
until <span class="inlinecode"><span class="id" type="var">X</span></span> reaches <span class="inlinecode">0</span>. So, if <span class="inlinecode"><span class="id" type="var">X</span></span> <span class="inlinecode">=</span> <span class="inlinecode">2</span> and <span class="inlinecode"><span class="id" type="var">Y</span></span> <span class="inlinecode">=</span> <span class="inlinecode">5</span> initially,
after one iteration of the loop we obtain <span class="inlinecode"><span class="id" type="var">X</span></span> <span class="inlinecode">=</span> <span class="inlinecode">1</span> and <span class="inlinecode"><span class="id" type="var">Y</span></span> <span class="inlinecode">=</span> <span class="inlinecode">4</span>;
after two iterations <span class="inlinecode"><span class="id" type="var">X</span></span> <span class="inlinecode">=</span> <span class="inlinecode">0</span> and <span class="inlinecode"><span class="id" type="var">Y</span></span> <span class="inlinecode">=</span> <span class="inlinecode">3</span>; and then the loop stops.
Notice that the difference between <span class="inlinecode"><span class="id" type="var">Y</span></span> and <span class="inlinecode"><span class="id" type="var">X</span></span> stays constant
between iterations; initially, <span class="inlinecode"><span class="id" type="var">Y</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">n</span></span> and <span class="inlinecode"><span class="id" type="var">X</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">m</span></span>, so this
difference is always <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">-</span> <span class="inlinecode"><span class="id" type="var">m</span></span>. So let's try instantiating <span class="inlinecode"><span class="id" type="var">I</span></span> in
the skeleton above with <span class="inlinecode"><span class="id" type="var">Y</span></span> <span class="inlinecode">-</span> <span class="inlinecode"><span class="id" type="var">X</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">-</span> <span class="inlinecode"><span class="id" type="var">m</span></span>.
<div class="paragraph"> </div>
<div class="code code-tight">
(1) <span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">X</span> = <span class="id" type="var">m</span> <span style="font-family: arial;">∧</span> <span class="id" type="var">Y</span> = <span class="id" type="var">n</span> <span style="letter-spacing:-.4em;">}</span>} <span style="font-family: arial;">⇾</span> (<span class="id" type="var">a</span> - <span class="id" type="var">OK</span>)<br/>
(2) <span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">Y</span> - <span class="id" type="var">X</span> = <span class="id" type="var">n</span> - <span class="id" type="var">m</span> <span style="letter-spacing:-.4em;">}</span>}<br/>
<span class="id" type="var">WHILE</span> <span class="id" type="var">X</span> ≠ 0 <span class="id" type="var">DO</span><br/>
(3) <span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">Y</span> - <span class="id" type="var">X</span> = <span class="id" type="var">n</span> - <span class="id" type="var">m</span> <span style="font-family: arial;">∧</span> <span class="id" type="var">X</span> ≠ 0 <span style="letter-spacing:-.4em;">}</span>} <span style="font-family: arial;">⇾</span> (<span class="id" type="var">c</span> - <span class="id" type="var">OK</span>)<br/>
(4) <span style="letter-spacing:-.4em;">{</span>{ (<span class="id" type="var">Y</span> - 1) - (<span class="id" type="var">X</span> - 1) = <span class="id" type="var">n</span> - <span class="id" type="var">m</span> <span style="letter-spacing:-.4em;">}</span>}<br/>
<span class="id" type="var">Y</span> ::= <span class="id" type="var">Y</span> - 1;<br/>
(5) <span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">Y</span> - (<span class="id" type="var">X</span> - 1) = <span class="id" type="var">n</span> - <span class="id" type="var">m</span> <span style="letter-spacing:-.4em;">}</span>}<br/>
<span class="id" type="var">X</span> ::= <span class="id" type="var">X</span> - 1<br/>
(6) <span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">Y</span> - <span class="id" type="var">X</span> = <span class="id" type="var">n</span> - <span class="id" type="var">m</span> <span style="letter-spacing:-.4em;">}</span>}<br/>
<span class="id" type="var">END</span><br/>
(7) <span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">Y</span> - <span class="id" type="var">X</span> = <span class="id" type="var">n</span> - <span class="id" type="var">m</span> <span style="font-family: arial;">∧</span> <span class="id" type="var">X</span> = 0 <span style="letter-spacing:-.4em;">}</span>} <span style="font-family: arial;">⇾</span> (<span class="id" type="var">b</span> - <span class="id" type="var">OK</span>)<br/>
(8) <span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">Y</span> = <span class="id" type="var">n</span> - <span class="id" type="var">m</span> <span style="letter-spacing:-.4em;">}</span>}
<div class="paragraph"> </div>
</div>
<div class="paragraph"> </div>
Success! Conditions (a), (b) and (c) all hold now. (To
verify (c), we need to check that, under the assumption that <span class="inlinecode"><span class="id" type="var">X</span></span> <span class="inlinecode">≠</span>
<span class="inlinecode">0</span>, we have <span class="inlinecode"><span class="id" type="var">Y</span></span> <span class="inlinecode">-</span> <span class="inlinecode"><span class="id" type="var">X</span></span> <span class="inlinecode">=</span> <span class="inlinecode">(<span class="id" type="var">Y</span></span> <span class="inlinecode">-</span> <span class="inlinecode">1)</span> <span class="inlinecode">-</span> <span class="inlinecode">(<span class="id" type="var">X</span></span> <span class="inlinecode">-</span> <span class="inlinecode">1)</span>; this holds for all
natural numbers <span class="inlinecode"><span class="id" type="var">X</span></span> and <span class="inlinecode"><span class="id" type="var">Y</span></span>.)
</div>
<div class="code code-tight">
<br/>
</div>
<div class="doc">
<a name="lab555"></a><h2 class="section">Exercise: Slow Assignment</h2>
<div class="paragraph"> </div>
<a name="lab556"></a><h4 class="section">Exercise: 2 stars (slow_assignment)</h4>
A roundabout way of assigning a number currently stored in <span class="inlinecode"><span class="id" type="var">X</span></span> to
the variable <span class="inlinecode"><span class="id" type="var">Y</span></span> is to start <span class="inlinecode"><span class="id" type="var">Y</span></span> at <span class="inlinecode">0</span>, then decrement <span class="inlinecode"><span class="id" type="var">X</span></span> until
it hits <span class="inlinecode">0</span>, incrementing <span class="inlinecode"><span class="id" type="var">Y</span></span> at each step. Here is a program that
implements this idea:
<div class="paragraph"> </div>
<div class="code code-tight">
<span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">X</span> = <span class="id" type="var">m</span> <span style="letter-spacing:-.4em;">}</span>}<br/>
<span class="id" type="var">Y</span> ::= 0;<br/>
<span class="id" type="var">WHILE</span> <span class="id" type="var">X</span> ≠ 0 <span class="id" type="var">DO</span><br/>
<span class="id" type="var">X</span> ::= <span class="id" type="var">X</span> - 1;<br/>
<span class="id" type="var">Y</span> ::= <span class="id" type="var">Y</span> + 1;<br/>
<span class="id" type="var">END</span><br/>
<span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">Y</span> = <span class="id" type="var">m</span> <span style="letter-spacing:-.4em;">}</span>}
<div class="paragraph"> </div>
</div>
Write an informal decorated program showing that this is correct.
</div>
<div class="code code-tight">
<br/>
<span class="comment">(* FILL IN HERE *)</span><br/>
</div>
<div class="doc">
<font size=-2>☐</font>
</div>
<div class="code code-tight">
<br/>
</div>
<div class="doc">
<a name="lab557"></a><h2 class="section">Exercise: Slow Addition</h2>
<div class="paragraph"> </div>
<a name="lab558"></a><h4 class="section">Exercise: 3 stars, optional (add_slowly_decoration)</h4>
The following program adds the variable X into the variable Z
by repeatedly decrementing X and incrementing Z.
<div class="paragraph"> </div>
<div class="code code-tight">
<span class="id" type="var">WHILE</span> <span class="id" type="var">X</span> ≠ 0 <span class="id" type="var">DO</span><br/>
<span class="id" type="var">Z</span> ::= <span class="id" type="var">Z</span> + 1;<br/>
<span class="id" type="var">X</span> ::= <span class="id" type="var">X</span> - 1<br/>
<span class="id" type="var">END</span>
<div class="paragraph"> </div>
</div>
<div class="paragraph"> </div>
Following the pattern of the <span class="inlinecode"><span class="id" type="var">subtract_slowly</span></span> example above, pick
a precondition and postcondition that give an appropriate
specification of <span class="inlinecode"><span class="id" type="var">add_slowly</span></span>; then (informally) decorate the
program accordingly.
</div>
<div class="code code-tight">
<br/>
<span class="comment">(* FILL IN HERE *)</span><br/>
</div>
<div class="doc">
<font size=-2>☐</font>
</div>
<div class="code code-tight">
<br/>
</div>
<div class="doc">
<a name="lab559"></a><h2 class="section">Example: Parity</h2>
<div class="paragraph"> </div>
Here is a cute little program for computing the parity of the
value initially stored in <span class="inlinecode"><span class="id" type="var">X</span></span> (due to Daniel Cristofani).
<div class="paragraph"> </div>
<div class="code code-tight">
<span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">X</span> = <span class="id" type="var">m</span> <span style="letter-spacing:-.4em;">}</span>}<br/>
<span class="id" type="var">WHILE</span> 2 ≤ <span class="id" type="var">X</span> <span class="id" type="var">DO</span><br/>
<span class="id" type="var">X</span> ::= <span class="id" type="var">X</span> - 2<br/>
<span class="id" type="var">END</span><br/>
<span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">X</span> = <span class="id" type="var">parity</span> <span class="id" type="var">m</span> <span style="letter-spacing:-.4em;">}</span>}
<div class="paragraph"> </div>
</div>
The mathematical <span class="inlinecode"><span class="id" type="var">parity</span></span> function used in the specification is
defined in Coq as follows:
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">parity</span> <span class="id" type="var">x</span> :=<br/>
<span class="id" type="keyword">match</span> <span class="id" type="var">x</span> <span class="id" type="keyword">with</span><br/>
| 0 ⇒ 0<br/>
| 1 ⇒ 1<br/>
| <span class="id" type="var">S</span> (<span class="id" type="var">S</span> <span class="id" type="var">x'</span>) ⇒ <span class="id" type="var">parity</span> <span class="id" type="var">x'</span><br/>
<span class="id" type="keyword">end</span>.<br/>
<br/>
</div>
<div class="doc">
The postcondition does not hold at the beginning of the loop,
since <span class="inlinecode"><span class="id" type="var">m</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">parity</span></span> <span class="inlinecode"><span class="id" type="var">m</span></span> does not hold for an arbitrary <span class="inlinecode"><span class="id" type="var">m</span></span>, so we
cannot use that as an invariant. To find an invariant that works,
let's think a bit about what this loop does. On each iteration it
decrements <span class="inlinecode"><span class="id" type="var">X</span></span> by <span class="inlinecode">2</span>, which preserves the parity of <span class="inlinecode"><span class="id" type="var">X</span></span>. So the
parity of <span class="inlinecode"><span class="id" type="var">X</span></span> does not change, i.e. it is invariant. The initial
value of <span class="inlinecode"><span class="id" type="var">X</span></span> is <span class="inlinecode"><span class="id" type="var">m</span></span>, so the parity of <span class="inlinecode"><span class="id" type="var">X</span></span> is always equal to the
parity of <span class="inlinecode"><span class="id" type="var">m</span></span>. Using <span class="inlinecode"><span class="id" type="var">parity</span></span> <span class="inlinecode"><span class="id" type="var">X</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">parity</span></span> <span class="inlinecode"><span class="id" type="var">m</span></span> as an invariant we
obtain the following decorated program:
<div class="paragraph"> </div>
<div class="code code-tight">
<span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">X</span> = <span class="id" type="var">m</span> <span style="letter-spacing:-.4em;">}</span>} <span style="font-family: arial;">⇾</span> (<span class="id" type="var">a</span> - <span class="id" type="var">OK</span>)<br/>
<span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">parity</span> <span class="id" type="var">X</span> = <span class="id" type="var">parity</span> <span class="id" type="var">m</span> <span style="letter-spacing:-.4em;">}</span>}<br/>
<span class="id" type="var">WHILE</span> 2 ≤ <span class="id" type="var">X</span> <span class="id" type="var">DO</span><br/>
<span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">parity</span> <span class="id" type="var">X</span> = <span class="id" type="var">parity</span> <span class="id" type="var">m</span> <span style="font-family: arial;">∧</span> 2 ≤ <span class="id" type="var">X</span> <span style="letter-spacing:-.4em;">}</span>} <span style="font-family: arial;">⇾</span> (<span class="id" type="var">c</span> - <span class="id" type="var">OK</span>)<br/>
<span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">parity</span> (<span class="id" type="var">X</span>-2) = <span class="id" type="var">parity</span> <span class="id" type="var">m</span> <span style="letter-spacing:-.4em;">}</span>}<br/>
<span class="id" type="var">X</span> ::= <span class="id" type="var">X</span> - 2<br/>
<span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">parity</span> <span class="id" type="var">X</span> = <span class="id" type="var">parity</span> <span class="id" type="var">m</span> <span style="letter-spacing:-.4em;">}</span>}<br/>
<span class="id" type="var">END</span><br/>
<span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">parity</span> <span class="id" type="var">X</span> = <span class="id" type="var">parity</span> <span class="id" type="var">m</span> <span style="font-family: arial;">∧</span> <span class="id" type="var">X</span> < 2 <span style="letter-spacing:-.4em;">}</span>} <span style="font-family: arial;">⇾</span> (<span class="id" type="var">b</span> - <span class="id" type="var">OK</span>)<br/>
<span style="letter-spacing:-.4em;">{</span>{ <span class="id" type="var">X</span> = <span class="id" type="var">parity</span> <span class="id" type="var">m</span> <span style="letter-spacing:-.4em;">}</span>}
<div class="paragraph"> </div>
</div>
<div class="paragraph"> </div>
With this invariant, conditions (a), (b), and (c) are all