7601:
501:.” It is fairly easy to adapt the axioms so that they cannot be used to predict the “results” of nonterminating programs; but the actual use of the axioms would now depend on knowledge of many implementation-dependent features, for example, the size and speed of the computer, the range of numbers, and the choice of overflow technique. Apart from proofs of the avoidance of infinite loops, it is probably better to prove the “conditional” correctness of a program and rely on an implementation to give a warning if it has had to abandon execution of the program as a result of violation of an implementation limit.
444:"Termination" here and in the rest of this article is meant in the broader sense that computation will eventually be finished, that is it implies the absence of infinite loops; it does not imply the absence of implementation limit violations (e.g. division by zero) stopping the program prematurely. In his 1969 paper, Hoare used a narrower notion of termination which also entailed the absence of implementation limit violations, and expressed his preference for the broader notion of termination as it keeps assertions implementation-independent:
8155:
8175:
8165:
3653:
3471:
3339:
448:
Another deficiency in the axioms and rules quoted above is that they give no basis for a proof that a program successfully terminates. Failure to terminate may be due to an infinite loop; or it may be due to violation of an implementation-defined limit, for example, the range of numeric operands, the
5631:
5969:
4050:
1324:
The assignment axiom scheme is equivalent to saying that to find the precondition, first take the post-condition and replace all occurrences of the left-hand side of the assignment with the right-hand side of the assignment. Be careful not to try to do this backwards by following this
3841:
7235:
5095:
5266:
3648:{\displaystyle {\texttt {bool}}\ b:={\texttt {true}};{\texttt {while}}\ B\wedge b\ {\texttt {do}}\ S;b:={\texttt {false}}\ {\texttt {done}};b:={\texttt {true}};{\texttt {while}}\ \neg B\wedge b\ {\texttt {do}}\ T;b:={\texttt {false}}\ {\texttt {done}}}
2064:
3182:
1952:
1846:
3460:
5713:
1740:
5520:
6254:
5760:
2944:
4142:
4308:
3917:
3693:
5346:
4505:
265:. In addition to the rules for the simple language in Hoare's original paper, rules for other language constructs have been developed since then by Hoare and many other researchers. There are rules for
4807:
4584:
4218:
4745:
7070:
4980:
579:
5152:
7001:
1593:
5461:
7067:
Hoare's 1969 paper didn't provide a total correctness rule; cf. his discussion on p.579 (top left). For example
Reynolds' textbook gives the following version of a total correctness rule:
7056:
4372:
1043:
5410:
3166:
672:
3018:
1510:
974:
7515:
4927:
3080:
589:
The assignment axiom states that, after the assignment, any predicate that was previously true for the right-hand side of the assignment now holds for the variable. Formally, let
2687:
2584:
4629:
2135:
1447:
4667:
2781:
2480:
8178:
6094:
1959:
8168:
4422:
3334:{\displaystyle {\dfrac {\{B\wedge P\}S\{Q\}\quad ,\quad \{\neg B\wedge P\}T\{Q\}}{\{P\}{\texttt {if}}\ B\ {\texttt {then}}\ S\ {\texttt {else}}\ T\ {\texttt {endif}}\{Q\}}}}
1388:
5754:, i.e. termination as well as partial correctness. Commonly, square brackets are used here instead of curly braces to indicate the different notion of program correctness.
6062:
6040:
6951:
119:
2369:
1853:
1747:
5493:
4959:
4897:
6913:
2627:
2523:
2407:
2251:
479:
7740:
6690:
6573:
6440:
5137:
2727:
1319:
1287:
1255:
1174:
1112:
1080:
894:
4865:
4838:
3898:
3871:
3393:
2219:
2176:
6469:
6291:
5650:
1142:
2832:
2325:
1647:
1637:
1223:
854:
813:
772:
712:
499:
439:
419:
399:
379:
359:
339:
319:
238:
212:
188:
162:
142:
6804:
6754:
5626:{\displaystyle \{{\texttt {true}}\}{\texttt {while}}\ x\cdot x\neq a\ {\texttt {do}}\ {\texttt {skip}}\ {\texttt {done}}\{x\cdot x=a\wedge {\texttt {true}}\}}
7938:
7837:
5964:{\displaystyle {\dfrac {<\ {\text{is a well-founded ordering on the set}}\ D\quad ,\quad S}{{\texttt {while}}\ B\ {\texttt {do}}\ S\ {\texttt {done}}}}}
6140:
7820:
2848:
4045:{\displaystyle \{0\leq x\leq 15\}{\texttt {if}}\ x<15\ {\texttt {then}}\ x:=x+1\ {\texttt {else}}\ x:=0\ {\texttt {endif}}\{0\leq x\leq 15\}}
4061:
4233:
301:, which can be proven separately or with an extended version of the While rule. Thus the intuitive reading of a Hoare triple is: Whenever
3836:{\displaystyle {\dfrac {P_{1}\rightarrow P_{2}\quad ,\quad \{P_{2}\}S\{Q_{2}\}\quad ,\quad Q_{2}\rightarrow Q_{1}}{\{P_{1}\}S\{Q_{1}\}}}}
7522:
1050:
All preconditions that are not modified by the expression can be carried over to the postcondition. In the first example, assigning
3658:
the conditional rule can be derived from the other Hoare rules. In a similar way, rules for other derived program constructs, like
7478:
5498:
For another example, the while rule can be used to formally verify the following strange program to compute the exact square root
5277:
4430:
2297:, respectively. The proof is best read backwards, starting from line 7; for example, line 5 is obtained from line 7 by replacing
7230:{\displaystyle {\dfrac {P\wedge B\rightarrow 0\leq t\quad ,\quad S}{{\texttt {while}}\ B\ {\texttt {do}}\ S\ {\texttt {done}}}}}
6471:
decreases in every loop cycle, while it always remains non-negative; this process can go on only for a finite number of cycles.
5090:{\displaystyle {\dfrac {\{P\wedge B\}S\{P\}}{\{P\}{\texttt {while}}\ B\ {\texttt {do}}\ S\ {\texttt {done}}\{\neg B\wedge P\}}}}
4752:
4512:
5261:{\displaystyle \{x\leq 10\}{\texttt {while}}\ x<10\ {\texttt {do}}\ x:=x+1\ {\texttt {done}}\{\neg x<10\wedge x\leq 10\}}
4149:
4682:
80:. A triple describes how the execution of a piece of code changes the state of the computation. A Hoare triple is of the form
533:
481:” should be interpreted “provided that the program successfully terminates, the properties of its results are described by
1114:, so both statements may appear in the postcondition. Formally, this result is obtained by applying the axiom schema with
4929:, respectively, to strengthen again the precondition. Informally, the effect of the consequence rule is to "forget" that
7388:
719:
598:
6969:
1518:
7777:
7456:
5419:
7030:
6127:
any further, i.e. the premise of the rule would be false. (This is one of various notations for total correctness.)
4315:
980:
8209:
6828:
5353:
3091:
46:
6096:; all these sets are meant in the mathematical, not in the computing sense, they are all infinite in particular.)
7876:
6858:
607:
246:: when the precondition is met, executing the command establishes the postcondition. Assertions are formulae in
8037:
7891:
7585:
7550:
278:
266:
2955:
1459:
911:
8127:
7600:
7336:" Proceedings of the American Mathematical Society Symposia on Applied Mathematics. Vol. 19, pp. 19–31. 1967.
8090:
7609:
7560:
270:
17:
8029:
4902:
3029:
8065:
7984:
6843:
2642:
2539:
2059:{\displaystyle \{0\leq y\cdot y\wedge y\cdot y\leq 9\}x:=y\cdot y\{0\leq y\cdot y\wedge y\cdot y\leq 9\}}
56:, and subsequently refined by Hoare and other researchers. The original ideas were seeded by the work of
4593:
2084:
1396:
8199:
8095:
7815:
4634:
2742:
2441:
6070:
8158:
7686:
7508:
7293:
4395:
1332:
8009:
7807:
6045:
6023:
1947:{\displaystyle \{0\leq y\cdot y\wedge y\cdot y\leq 9\}x:=y\cdot y\{0\leq y\cdot y\wedge x\leq 9\}}
1841:{\displaystyle \{0\leq y\cdot y\wedge y\cdot y\leq 9\}x:=y\cdot y\{0\leq x\wedge y\cdot y\leq 9\}}
7969:
7725:
7717:
6918:
6863:
274:
86:
8204:
8112:
8107:
7910:
7629:
6833:
3679:
2330:
262:
5466:
4932:
4870:
3455:{\displaystyle {\texttt {if}}\ B\ {\texttt {then}}\ S\ {\texttt {else}}\ T\ {\texttt {endif}}}
7735:
7641:
7634:
6886:
6065:
5987:
5708:{\displaystyle \{{\texttt {true}}\wedge x\cdot x\neq a\}{\texttt {skip}}\{{\texttt {true}}\}}
2597:
2493:
2374:
2224:
452:
166:
7261:
is an integer expression (Reynolds' variables renamed to fit with this article's settings).
6585:
6480:
6299:
5119:
2700:
1292:
1260:
1228:
1147:
1085:
1053:
859:
7905:
7900:
7787:
7663:
7651:
7580:
6818:
can be found that is decreased by the empty loop body, hence termination cannot be proved.
6002:
4843:
4816:
3876:
3849:
2181:
2155:
2149:
1735:{\displaystyle \{0\leq y\cdot y\wedge y\cdot y\leq 9\}x:=y\cdot y\{0\leq x\wedge x\leq 9\}}
727:
298:
7333:
6448:
6270:
1121:
8:
7917:
7752:
7624:
6848:
3387:
This rule was not contained in Hoare's original publication. However, since a statement
2811:
2304:
2281:, without needing an auxiliary variable. In the verification proof, the initial value of
290:
7497:) – A visualisation of the Hoare calculus in the algorithm visualisation program j-Algo.
2327:(source expression in line 6). Some arithmetical simplifications are used tacitly, viz.
7886:
7827:
7797:
7782:
7747:
7646:
7590:
7545:
7425:
7312:
7027:
is called its succedent. A rule without antecedents is called an axiom, and written as
6838:
1605:
1179:
822:
781:
740:
680:
484:
424:
404:
384:
364:
344:
324:
304:
223:
197:
173:
147:
127:
50:
6759:
6697:
8001:
7575:
7452:
7429:
7384:
7316:
6963:
5975:
5751:
294:
7468:
6249:{\displaystyle {\texttt {while}}\ x<10\ {\texttt {do}}\ x:=x+1\ {\texttt {done}}}
523:
statement does not change the state of the program, thus whatever holds true before
7948:
7847:
7772:
7681:
7531:
7417:
7378:
7349:
7302:
8052:
7842:
7762:
7671:
7329:
6112:
247:
57:
8070:
7953:
7881:
7861:
7767:
7730:
7696:
7565:
7421:
6853:
5750:
is replaced by the following one, the Hoare calculus can also be used to prove
5734:'s square root. In all other cases, it will not terminate; therefore it is not
5105:
2273:
The three statements below (line 2, 4, 6) exchange the values of the variables
258:
2152:), although it is a proper instance of the assignment axiom scheme (with both
8193:
7757:
7691:
7555:
5974:
In this rule, in addition to maintaining the loop invariant, one also proves
2939:{\displaystyle {\dfrac {\{P\}S\{Q\}\quad ,\quad \{Q\}T\{R\}}{\{P\}S;T\{R\}}}}
242:
42:
5416:
which is easily obtained by the assignment rule. Finally, the postcondition
8117:
8100:
7943:
7570:
7490:
7451:(a textbook that includes an introduction to Hoare logic, written in 2002)
7284:
5983:
2949:
For example, consider the following two instances of the assignment axiom:
216:
7447:
7307:
7288:
7792:
7494:
7475:
theorem prover. It features a Hoare calculus for a simple while language.
6263:
being the non-negative integers with the usual order, and the expression
2078:
when more than one name may refer to the same stored value. For example,
4137:{\displaystyle \{0\leq x\leq 15\wedge x<15\}x:=x+1\{0\leq x\leq 15\}}
3900:. It is used e.g. to achieve literally identical postconditions for the
8019:
8014:
4303:{\displaystyle \{0\leq x\leq 15\wedge x\geq 15\}x:=0\{0\leq x\leq 15\}}
516:
449:
size of storage, or an operating system time limit. Thus the notation “
53:
2792:
Hoare's rule of composition applies to sequentially executed programs
8080:
7896:
7676:
4055:
needs to apply the conditional rule, which in turn requires to prove
61:
7482:
7979:
7500:
7974:
7832:
6018:
381:
does not terminate. In the latter case, there is no "after", so
49:. It was proposed in 1969 by the British computer scientist and
7486:
45:
with a set of logical rules for reasoning rigorously about the
7405:
6259:
the while rule for total correctness can be applied with e.g.
6013:
cannot keep decreasing forever. (For example, the usual order
5139:
must have caused the loop to end. As in the conditional rule,
4590:
The consequence rule is needed to strengthen the precondition
8132:
8122:
8042:
1289:), which can in turn be simplified to the given precondition
254:
7471:
is a semi-automatic verification system built on top of the
5341:{\displaystyle \{x\leq 10\wedge x<10\}x:=x+1\{x\leq 10\}}
4500:{\displaystyle \{0\leq x+1\leq 15\}x:=x+1\{0\leq x\leq 15\}}
815:
true prior to the assignment, by the assignment axiom, then
8085:
8060:
7404:
Apt, Krzysztof R.; Olderog, Ernst-RĂĽdiger (December 2019).
5719:
which follows from the skip rule and the consequence rule.
4802:{\displaystyle \{{\texttt {true}}\}x:=0\{0\leq x\leq 15\}}
4579:{\displaystyle \{-1\leq x<15\}x:=x+1\{0\leq x\leq 15\}}
7472:
5726:
correct: if it happened to terminate, it is certain that
4213:{\displaystyle \{0\leq x<15\}x:=x+1\{0\leq x\leq 15\}}
3380:, must not have side effects. An example is given in the
6445:
Informally speaking, we have to prove that the distance
4740:{\displaystyle \{0\leq 0\leq 15\}x:=0\{0\leq x\leq 15\}}
8075:
574:{\displaystyle {\dfrac {}{\{P\}{\texttt {skip}}\{P\}}}}
7075:
7073:
7035:
7033:
6974:
6972:
6921:
6889:
6762:
6700:
6588:
6483:
6451:
6302:
6273:
6143:
6073:
6048:
6026:
5765:
5763:
5653:
5523:
5469:
5422:
5356:
5280:
5155:
5122:
4985:
4983:
4935:
4905:
4873:
4846:
4819:
4755:
4685:
4637:
4596:
4515:
4433:
4398:
4318:
4236:
4152:
4064:
3920:
3879:
3852:
3698:
3696:
3474:
3396:
3187:
3185:
3094:
3032:
2958:
2853:
2851:
2814:
2745:
2703:
2645:
2600:
2542:
2496:
2444:
2377:
2333:
2307:
2227:
2184:
2158:
2087:
1962:
1856:
1750:
1650:
1608:
1521:
1462:
1399:
1335:
1295:
1263:
1231:
1182:
1150:
1124:
1088:
1056:
983:
914:
862:
825:
784:
743:
683:
612:
610:
538:
536:
487:
455:
427:
407:
387:
367:
347:
327:
307:
226:
200:
176:
150:
130:
89:
2071:
are valid instances of the assignment axiom scheme.
819:
would be true subsequent to which. Conversely, were
737:
The assignment axiom scheme means that the truth of
401:
can be any statement at all. Indeed, one can choose
5986:, whose value strictly decreases with respect to a
5741:
7241:is an integer variable that doesn't occur free in
7229:
7050:
6995:
6945:
6907:
6798:
6748:
6684:
6567:
6463:
6434:
6285:
6248:
6088:
6056:
6034:
5963:
5707:
5625:
5487:
5455:
5404:
5340:
5260:
5131:
5089:
4953:
4921:
4891:
4859:
4832:
4813:hence the consequence rule has to be applied with
4801:
4739:
4661:
4623:
4578:
4499:
4416:
4366:
4302:
4212:
4136:
4044:
3892:
3865:
3835:
3647:
3454:
3333:
3160:
3074:
3012:
2938:
2826:
2775:
2721:
2681:
2621:
2578:
2517:
2474:
2401:
2363:
2319:
2245:
2213:
2170:
2129:
2058:
1946:
1840:
1734:
1631:
1587:
1504:
1441:
1382:
1313:
1281:
1249:
1217:
1168:
1136:
1106:
1074:
1037:
968:
888:
848:
807:
766:
706:
666:
573:
493:
473:
433:
413:
393:
373:
353:
333:
313:
232:
206:
182:
156:
136:
113:
3465:has the same effect as a one-time loop construct
3344:The conditional rule states that a postcondition
8191:
7348:
6996:{\displaystyle {\dfrac {\alpha ,\beta }{\phi }}}
3846:This rule allows to strengthen the precondition
1588:{\displaystyle \{x=5\}x:=x+1\{x=5\wedge x=x+1\}}
1390:; this rule leads to nonsensical examples like:
284:
7344:
7342:
5456:{\displaystyle \{\neg x<10\wedge x\leq 10\}}
774:is equivalent to the after-assignment truth of
510:
7051:{\displaystyle {\dfrac {}{\quad \phi \quad }}}
4367:{\displaystyle \{x=15\}x:=0\{0\leq x\leq 15\}}
1038:{\displaystyle \{x+1\leq N\}x:=x+1\{x\leq N\}}
7516:
7289:"An axiomatic basis for computer programming"
6474:The previous proof goal can be simplified to
5730:must have contained (by chance) the value of
5405:{\displaystyle \{x<10\}x:=x+1\{x\leq 10\}}
5112:. After the loop is finished, this invariant
4965:part, since the assignment rule used for the
3161:{\displaystyle \{x+1=43\}y:=x+1;z:=y\{z=43\}}
7339:
6940:
6934:
6928:
6922:
6899:
6893:
5702:
5692:
5682:
5654:
5620:
5592:
5534:
5524:
5482:
5470:
5450:
5423:
5399:
5387:
5369:
5357:
5335:
5323:
5305:
5281:
5255:
5228:
5168:
5156:
5108:, which is to be preserved by the loop body
5080:
5065:
5023:
5017:
5012:
5006:
5000:
4988:
4948:
4936:
4916:
4906:
4886:
4874:
4796:
4778:
4766:
4756:
4734:
4716:
4704:
4686:
4656:
4638:
4618:
4597:
4573:
4555:
4537:
4516:
4494:
4476:
4458:
4434:
4361:
4343:
4331:
4319:
4297:
4279:
4267:
4237:
4207:
4189:
4171:
4153:
4131:
4113:
4095:
4065:
4039:
4021:
3939:
3921:
3826:
3813:
3807:
3794:
3761:
3748:
3742:
3729:
3324:
3318:
3260:
3254:
3249:
3243:
3237:
3222:
3214:
3208:
3202:
3190:
3155:
3143:
3113:
3095:
3069:
3057:
3045:
3033:
3007:
2995:
2977:
2959:
2929:
2923:
2911:
2905:
2900:
2894:
2888:
2882:
2874:
2868:
2862:
2856:
2770:
2746:
2676:
2646:
2573:
2543:
2469:
2445:
2240:
2228:
2208:
2185:
2165:
2159:
2124:
2112:
2100:
2088:
2053:
2017:
1999:
1963:
1941:
1911:
1893:
1857:
1835:
1805:
1787:
1751:
1729:
1705:
1687:
1651:
1582:
1552:
1534:
1522:
1499:
1481:
1469:
1463:
1436:
1424:
1412:
1400:
1377:
1354:
1342:
1336:
1032:
1020:
1002:
984:
963:
951:
933:
915:
657:
651:
639:
616:
564:
558:
548:
542:
465:
459:
108:
102:
96:
90:
27:Rules to verify computer program correctness
3171:Another example is shown in the right box.
667:{\displaystyle {\dfrac {}{\{P\}x:=E\{P\}}}}
321:holds of the state before the execution of
8174:
8164:
7523:
7509:
7403:
3682:to the rules from Hoare's original paper.
3368:part, the unnegated and negated condition
3356:part is also a postcondition of the whole
584:
7306:
6076:
6050:
6028:
4507:, which is logically equivalent to
1639:, the converse is not true. For example:
1512:; it leads to nonsensical examples like:
1456:rule looking tempting at first glance is
896:true) prior to the assignment statement,
60:, who had published a similar system for
7377:Huth, Michael; Ryan, Mark (2004-08-26).
7376:
7200:
7184:
7168:
6211:
6183:
6161:
5922:
5906:
5890:
5697:
5687:
5659:
5615:
5587:
5577:
5567:
5539:
5529:
5223:
5195:
5173:
5060:
5044:
5028:
4911:
4761:
4016:
3994:
3966:
3944:
3640:
3630:
3608:
3583:
3573:
3557:
3547:
3525:
3503:
3493:
3477:
3447:
3431:
3415:
3399:
3313:
3297:
3281:
3265:
3013:{\displaystyle \{x+1=43\}y:=x+1\{y=43\}}
1505:{\displaystyle \{P\}x:=E\{P\wedge x=E\}}
969:{\displaystyle \{x+1=43\}y:=x+1\{y=43\}}
553:
7279:
7277:
6966:style notation for rules. For example,
6692:is obtained by the assignment rule, and
6293:, which then in turn requires to prove
6001:is well-founded, a strictly decreasing
3085:By the sequencing rule, one concludes:
2074:The assignment axiom proposed by Hoare
14:
8192:
2256:
593:be an assertion in which the variable
7504:
7383:(second ed.). CUP. p. 276.
7283:
5776:is a well-founded ordering on the set
4631:obtained from the assignment rule to
4384:However, the assignment rule for the
3381:
1602:uniquely determines the precondition
7530:
7274:
7023:are called antecedents of the rule,
5271:by the while rule requires to prove
4969:part doesn't need that information.
4922:{\displaystyle \{{\texttt {true}}\}}
3075:{\displaystyle \{y=43\}z:=y\{z=43\}}
6134:, for a total-correctness proof of
5636:After applying the while rule with
4669:required for the conditional rule.
3873:and/or to weaken the postcondition
3685:
3174:
2682:{\displaystyle \{b=A\wedge a-b=B\}}
2579:{\displaystyle \{a-b=A\wedge b=B\}}
903:Examples of valid triples include:
261:for all the constructs of a simple
24:
7439:
7214:
6219:
6130:Resuming the first example of the
5930:
5426:
5231:
5123:
5068:
4624:{\displaystyle \{-1\leq x<15\}}
3591:
3225:
2130:{\displaystyle \{y=3\}x:=2\{y=3\}}
1442:{\displaystyle \{x=5\}x:=3\{3=5\}}
863:
25:
8221:
7462:
7354:Theories of Programming Languages
4676:part, the assignment rule yields
4662:{\displaystyle \{0\leq x<15\}}
3372:can be added to the precondition
2776:{\displaystyle \{b=A\wedge a=B\}}
2475:{\displaystyle \{a=A\wedge b=B\}}
2301:(target expression in line 6) by
289:Using standard Hoare logic, only
8173:
8163:
8154:
8153:
7599:
6829:Assertion (software development)
6579:which can be proven as follows:
6089:{\displaystyle \mathbb {R} ^{+}}
6009:can have only finite length, so
5742:While rule for total correctness
5722:In fact, the strange program is
4424:; rule application hence yields
47:correctness of computer programs
7334:Assigning meanings to programs.
7103:
7099:
7043:
7039:
6859:Predicate transformer semantics
6811:
6131:
5789:
5785:
5747:
3768:
3764:
3728:
3724:
3376:, respectively. The condition,
3221:
3217:
2881:
2877:
900:must then be false afterwards.
263:imperative programming language
67:
7406:"Fifty years of Hoare's logic"
7397:
7370:
7361:
7323:
7220:
7205:
7163:
7157:
7152:
7134:
7128:
7104:
7087:
7061:
6956:
6877:
6810:For the second example of the
6793:
6763:
6743:
6701:
6679:
6649:
6631:
6589:
6562:
6532:
6514:
6484:
6429:
6381:
6363:
6303:
6243:
6216:
6156:
6144:
6042:, but neither on the integers
5954:
5927:
5885:
5867:
5862:
5832:
5826:
5790:
4417:{\displaystyle 0\leq x\leq 15}
3779:
3711:
2352:
2340:
2260:
2205:
2191:
1626:
1612:
1383:{\displaystyle \{P\}x:=E\{P\}}
1374:
1360:
1212:
1201:
1189:
1186:
1082:does not change the fact that
883:
869:
843:
829:
802:
788:
761:
747:
701:
687:
636:
622:
13:
1:
7356:. Cambridge University Press.
7268:
5997:during each iteration. Since
4972:
4961:is known at the entry of the
285:Partial and total correctness
7479:j-Algo Hoare Calculus module
6057:{\displaystyle \mathbb {Z} }
6035:{\displaystyle \mathbb {N} }
6017:is well-founded on positive
5143:must not have side effects.
2266:without auxiliary variables
2148:refer to the same variable (
1598:While a given postcondition
527:also holds true afterwards.
511:Empty statement axiom schema
421:to be false to express that
7:
7877:Curry–Howard correspondence
7410:Formal Aspects of Computing
6946:{\displaystyle \{P\}C\{Q\}}
6821:
5510:is an integer variable and
2289:is denoted by the constant
114:{\displaystyle \{P\}C\{Q\}}
10:
8226:
7422:10.1007/s00165-019-00501-3
7003:informally means "If both
6814:, of course no expression
5116:still holds, and moreover
8149:
8051:
8028:
8000:
7993:
7962:
7926:
7869:
7860:
7806:
7716:
7709:
7662:
7617:
7608:
7597:
7538:
7380:Logic in Computer Science
7358:) Here: Sect. 3.4, p. 64.
7294:Communications of the ACM
6119:, for otherwise the body
6099:Given the loop invariant
5748:above ordinary while rule
5146:For example, a proof of
2423:
2364:{\displaystyle a-(a-b)=b}
361:will hold afterwards, or
6883:Hoare originally wrote "
6870:
6806:by the consequence rule.
5978:by way of an expression
5514:is not a square number:
5488:{\displaystyle \{x=10\}}
4954:{\displaystyle \{x=15\}}
4892:{\displaystyle \{x=15\}}
4747:, or equivalently
4388:part requires to choose
3911:For example, a proof of
505:
8210:Static program analysis
7726:Abstract interpretation
7367:Hoare (1969), p.578-579
6908:{\displaystyle P\{C\}Q}
6864:Static program analysis
6756:can be strengthened to
5502:of an arbitrary number
2622:{\displaystyle b:=a-b;}
2518:{\displaystyle a:=a+b;}
2402:{\displaystyle a+b-b=a}
2246:{\displaystyle \{y=3\}}
585:Assignment axiom schema
474:{\displaystyle P\{Q\}R}
72:The central feature of
35:Floyd–Hoare logic
7231:
7052:
6997:
6947:
6909:
6834:Denotational semantics
6800:
6750:
6686:
6685:{\displaystyle x:=x+1}
6569:
6568:{\displaystyle x:=x+1}
6465:
6436:
6435:{\displaystyle x:=x+1}
6287:
6250:
6090:
6058:
6036:
5965:
5709:
5644:, it remains to prove
5627:
5489:
5457:
5406:
5348:, or simplified
5342:
5262:
5133:
5132:{\displaystyle \neg B}
5091:
4955:
4923:
4893:
4861:
4834:
4803:
4741:
4663:
4625:
4580:
4501:
4418:
4368:
4310:, or simplified
4304:
4214:
4144:, or simplified
4138:
4046:
3894:
3867:
3837:
3680:program transformation
3649:
3456:
3335:
3162:
3076:
3014:
2940:
2828:
2777:
2723:
2722:{\displaystyle a:=a-b}
2683:
2623:
2580:
2519:
2476:
2403:
2365:
2321:
2247:
2215:
2172:
2131:
2060:
1948:
1842:
1736:
1633:
1589:
1506:
1443:
1384:
1315:
1314:{\displaystyle x+1=43}
1283:
1282:{\displaystyle x+1=43}
1251:
1250:{\displaystyle x+1=43}
1219:
1170:
1169:{\displaystyle x+1=43}
1138:
1108:
1107:{\displaystyle x+1=43}
1076:
1075:{\displaystyle y:=x+1}
1039:
970:
890:
889:{\displaystyle \neg P}
850:
809:
768:
714:denotes the assertion
708:
668:
575:
519:rule asserts that the
503:
495:
475:
435:
415:
395:
375:
355:
335:
315:
297:additionally requires
234:
208:
184:
158:
138:
115:
7635:Categorical semantics
7308:10.1145/363235.363259
7232:
7053:
6998:
6948:
6910:
6801:
6751:
6687:
6570:
6466:
6437:
6288:
6251:
6091:
6066:positive real numbers
6059:
6037:
5988:well-founded relation
5966:
5710:
5628:
5490:
5463:can be simplified to
5458:
5407:
5343:
5263:
5134:
5092:
4956:
4924:
4894:
4862:
4860:{\displaystyle P_{2}}
4835:
4833:{\displaystyle P_{1}}
4804:
4742:
4664:
4626:
4581:
4502:
4419:
4369:
4305:
4215:
4139:
4047:
3895:
3893:{\displaystyle Q_{2}}
3868:
3866:{\displaystyle P_{2}}
3838:
3650:
3457:
3336:
3163:
3077:
3015:
2941:
2829:
2778:
2724:
2684:
2624:
2581:
2525:
2520:
2477:
2404:
2366:
2322:
2248:
2216:
2214:{\displaystyle \{P\}}
2173:
2171:{\displaystyle \{P\}}
2132:
2061:
1949:
1843:
1737:
1634:
1590:
1507:
1444:
1385:
1316:
1284:
1252:
1220:
1171:
1139:
1109:
1077:
1040:
971:
891:
851:
810:
769:
709:
669:
576:
496:
476:
446:
436:
416:
396:
376:
356:
336:
316:
253:Hoare logic provides
235:
209:
185:
159:
139:
116:
7581:Runtime verification
7071:
7031:
6970:
6962:This article uses a
6919:
6887:
6760:
6698:
6586:
6481:
6464:{\displaystyle 10-x}
6449:
6300:
6286:{\displaystyle 10-x}
6271:
6141:
6071:
6046:
6024:
5761:
5651:
5521:
5467:
5420:
5354:
5278:
5153:
5120:
4981:
4933:
4903:
4871:
4844:
4817:
4753:
4683:
4635:
4594:
4513:
4431:
4396:
4316:
4234:
4150:
4062:
3918:
3877:
3850:
3694:
3472:
3394:
3183:
3092:
3030:
2956:
2849:
2812:
2743:
2701:
2643:
2598:
2540:
2494:
2442:
2434:
2375:
2331:
2305:
2225:
2182:
2156:
2085:
1960:
1854:
1748:
1648:
1606:
1519:
1460:
1397:
1333:
1293:
1261:
1229:
1180:
1148:
1137:{\displaystyle y=43}
1122:
1086:
1054:
981:
912:
860:
823:
782:
741:
681:
608:
534:
485:
453:
441:does not terminate.
425:
405:
385:
365:
345:
325:
305:
224:
198:
174:
148:
128:
87:
7838:Invariant inference
7586:Safety and liveness
7448:Specifying Software
7445:Robert D. Tennent.
6849:Formal verification
6123:could not decrease
5993:on some domain set
4672:Similarly, for the
2827:{\displaystyle S;T}
2410:
2320:{\displaystyle a-b}
2264:Verifying swap-code
2257:Rule of composition
291:partial correctness
8002:Constraint solvers
7828:Concolic execution
7783:Symbolic execution
7591:Undefined behavior
7546:Control-flow graph
7227:
7225:
7048:
7046:
6993:
6991:
6943:
6905:
6839:Design by contract
6796:
6746:
6682:
6565:
6461:
6432:
6283:
6246:
6086:
6054:
6032:
5961:
5959:
5705:
5623:
5485:
5453:
5402:
5338:
5258:
5129:
5087:
5085:
4951:
4919:
4889:
4857:
4830:
4799:
4737:
4659:
4621:
4576:
4497:
4414:
4364:
4300:
4210:
4134:
4042:
3890:
3863:
3833:
3831:
3678:can be reduced by
3645:
3452:
3360:statement. In the
3331:
3329:
3158:
3072:
3010:
2936:
2934:
2824:
2804:executes prior to
2773:
2719:
2679:
2619:
2576:
2515:
2472:
2399:
2361:
2317:
2272:
2243:
2211:
2168:
2127:
2056:
1944:
1838:
1732:
1629:
1585:
1502:
1439:
1380:
1311:
1279:
1247:
1215:
1166:
1134:
1104:
1072:
1035:
966:
886:
846:
805:
764:
730:by the expression
704:
664:
662:
571:
569:
491:
471:
431:
411:
391:
371:
351:
331:
311:
230:
204:
180:
154:
134:
111:
8200:1969 in computing
8187:
8186:
8145:
8144:
8141:
8140:
7856:
7855:
7705:
7704:
7224:
7202:
7197:
7191:
7186:
7181:
7175:
7170:
7045:
7037:
6990:
6964:natural deduction
6213:
6208:
6190:
6185:
6180:
6168:
6163:
5958:
5924:
5919:
5913:
5908:
5903:
5897:
5892:
5781:
5777:
5773:
5752:total correctness
5699:
5689:
5661:
5617:
5589:
5584:
5579:
5574:
5569:
5564:
5546:
5541:
5531:
5225:
5220:
5202:
5197:
5192:
5180:
5175:
5084:
5062:
5057:
5051:
5046:
5041:
5035:
5030:
4913:
4763:
4018:
4013:
4001:
3996:
3991:
3973:
3968:
3963:
3951:
3946:
3830:
3642:
3637:
3632:
3615:
3610:
3605:
3590:
3585:
3575:
3559:
3554:
3549:
3532:
3527:
3522:
3510:
3505:
3495:
3484:
3479:
3449:
3444:
3438:
3433:
3428:
3422:
3417:
3412:
3406:
3401:
3328:
3315:
3310:
3304:
3299:
3294:
3288:
3283:
3278:
3272:
3267:
2933:
2790:
2789:
2786:
2785:
1632:{\displaystyle P}
1329:way of thinking:
1218:{\displaystyle P}
849:{\displaystyle P}
808:{\displaystyle P}
767:{\displaystyle P}
707:{\displaystyle P}
661:
614:
568:
555:
540:
494:{\displaystyle R}
434:{\displaystyle C}
414:{\displaystyle Q}
394:{\displaystyle Q}
374:{\displaystyle C}
354:{\displaystyle Q}
334:{\displaystyle C}
314:{\displaystyle P}
295:Total correctness
233:{\displaystyle Q}
207:{\displaystyle P}
183:{\displaystyle C}
157:{\displaystyle Q}
137:{\displaystyle P}
16:(Redirected from
8217:
8177:
8176:
8167:
8166:
8157:
8156:
8053:Proof assistants
7998:
7997:
7867:
7866:
7714:
7713:
7687:Rewriting system
7682:Process calculus
7615:
7614:
7603:
7532:Program analysis
7525:
7518:
7511:
7502:
7501:
7434:
7433:
7401:
7395:
7394:
7374:
7368:
7365:
7359:
7357:
7350:John C. Reynolds
7346:
7337:
7327:
7321:
7320:
7310:
7287:(October 1969).
7281:
7262:
7260:
7256:
7252:
7248:
7244:
7240:
7236:
7234:
7233:
7228:
7226:
7223:
7204:
7203:
7195:
7189:
7188:
7187:
7179:
7173:
7172:
7171:
7155:
7076:
7065:
7059:
7057:
7055:
7054:
7049:
7047:
7044:
7036:
7026:
7022:
7018:
7014:
7011:hold, then also
7010:
7006:
7002:
7000:
6999:
6994:
6992:
6986:
6975:
6960:
6954:
6952:
6950:
6949:
6944:
6914:
6912:
6911:
6906:
6881:
6817:
6812:previous section
6805:
6803:
6802:
6799:{\displaystyle }
6797:
6755:
6753:
6752:
6749:{\displaystyle }
6747:
6691:
6689:
6688:
6683:
6574:
6572:
6571:
6566:
6470:
6468:
6467:
6462:
6441:
6439:
6438:
6433:
6292:
6290:
6289:
6284:
6266:
6262:
6255:
6253:
6252:
6247:
6215:
6214:
6206:
6188:
6187:
6186:
6178:
6166:
6165:
6164:
6132:previous section
6126:
6122:
6118:
6110:
6107:must imply that
6106:
6103:, the condition
6102:
6095:
6093:
6092:
6087:
6085:
6084:
6079:
6063:
6061:
6060:
6055:
6053:
6041:
6039:
6038:
6033:
6031:
6016:
6012:
6008:
6000:
5996:
5992:
5981:
5970:
5968:
5967:
5962:
5960:
5957:
5926:
5925:
5917:
5911:
5910:
5909:
5901:
5895:
5894:
5893:
5865:
5779:
5778:
5775:
5771:
5766:
5733:
5729:
5714:
5712:
5711:
5706:
5701:
5700:
5691:
5690:
5663:
5662:
5643:
5639:
5632:
5630:
5629:
5624:
5619:
5618:
5591:
5590:
5582:
5581:
5580:
5572:
5571:
5570:
5562:
5544:
5543:
5542:
5533:
5532:
5513:
5509:
5505:
5501:
5494:
5492:
5491:
5486:
5462:
5460:
5459:
5454:
5411:
5409:
5408:
5403:
5347:
5345:
5344:
5339:
5267:
5265:
5264:
5259:
5227:
5226:
5218:
5200:
5199:
5198:
5190:
5178:
5177:
5176:
5142:
5138:
5136:
5135:
5130:
5115:
5111:
5103:
5096:
5094:
5093:
5088:
5086:
5083:
5064:
5063:
5055:
5049:
5048:
5047:
5039:
5033:
5032:
5031:
5015:
4986:
4968:
4964:
4960:
4958:
4957:
4952:
4928:
4926:
4925:
4920:
4915:
4914:
4898:
4896:
4895:
4890:
4866:
4864:
4863:
4858:
4856:
4855:
4839:
4837:
4836:
4831:
4829:
4828:
4808:
4806:
4805:
4800:
4765:
4764:
4746:
4744:
4743:
4738:
4675:
4668:
4666:
4665:
4660:
4630:
4628:
4627:
4622:
4585:
4583:
4582:
4577:
4506:
4504:
4503:
4498:
4423:
4421:
4420:
4415:
4391:
4387:
4380:
4373:
4371:
4370:
4365:
4309:
4307:
4306:
4301:
4226:
4219:
4217:
4216:
4211:
4143:
4141:
4140:
4135:
4051:
4049:
4048:
4043:
4020:
4019:
4011:
3999:
3998:
3997:
3989:
3971:
3970:
3969:
3961:
3949:
3948:
3947:
3907:
3903:
3899:
3897:
3896:
3891:
3889:
3888:
3872:
3870:
3869:
3864:
3862:
3861:
3842:
3840:
3839:
3834:
3832:
3829:
3825:
3824:
3806:
3805:
3792:
3791:
3790:
3778:
3777:
3760:
3759:
3741:
3740:
3723:
3722:
3710:
3709:
3699:
3686:Consequence rule
3677:
3673:
3669:
3665:
3661:
3654:
3652:
3651:
3646:
3644:
3643:
3635:
3634:
3633:
3613:
3612:
3611:
3603:
3588:
3587:
3586:
3577:
3576:
3561:
3560:
3552:
3551:
3550:
3530:
3529:
3528:
3520:
3508:
3507:
3506:
3497:
3496:
3482:
3481:
3480:
3461:
3459:
3458:
3453:
3451:
3450:
3442:
3436:
3435:
3434:
3426:
3420:
3419:
3418:
3410:
3404:
3403:
3402:
3379:
3375:
3371:
3367:
3363:
3359:
3355:
3351:
3347:
3340:
3338:
3337:
3332:
3330:
3327:
3317:
3316:
3308:
3302:
3301:
3300:
3292:
3286:
3285:
3284:
3276:
3270:
3269:
3268:
3252:
3188:
3175:Conditional rule
3167:
3165:
3164:
3159:
3081:
3079:
3078:
3073:
3019:
3017:
3016:
3011:
2945:
2943:
2942:
2937:
2935:
2932:
2903:
2854:
2837:
2833:
2831:
2830:
2825:
2807:
2803:
2799:
2795:
2782:
2780:
2779:
2774:
2728:
2726:
2725:
2720:
2688:
2686:
2685:
2680:
2628:
2626:
2625:
2620:
2585:
2583:
2582:
2577:
2524:
2522:
2521:
2516:
2481:
2479:
2478:
2473:
2411:
2408:
2406:
2405:
2400:
2371:(line 5→3), and
2370:
2368:
2367:
2362:
2326:
2324:
2323:
2318:
2300:
2296:
2292:
2288:
2284:
2280:
2276:
2271:
2261:
2252:
2250:
2249:
2244:
2220:
2218:
2217:
2212:
2201:
2177:
2175:
2174:
2169:
2147:
2143:
2136:
2134:
2133:
2128:
2065:
2063:
2062:
2057:
1953:
1951:
1950:
1945:
1847:
1845:
1844:
1839:
1741:
1739:
1738:
1733:
1638:
1636:
1635:
1630:
1622:
1601:
1594:
1592:
1591:
1586:
1511:
1509:
1508:
1503:
1448:
1446:
1445:
1440:
1389:
1387:
1386:
1381:
1370:
1320:
1318:
1317:
1312:
1288:
1286:
1285:
1280:
1256:
1254:
1253:
1248:
1224:
1222:
1221:
1216:
1208:
1176:), which yields
1175:
1173:
1172:
1167:
1143:
1141:
1140:
1135:
1117:
1113:
1111:
1110:
1105:
1081:
1079:
1078:
1073:
1044:
1042:
1041:
1036:
975:
973:
972:
967:
899:
895:
893:
892:
887:
879:
855:
853:
852:
847:
839:
818:
814:
812:
811:
806:
798:
777:
773:
771:
770:
765:
757:
733:
725:
717:
713:
711:
710:
705:
697:
673:
671:
670:
665:
663:
660:
632:
613:
596:
592:
580:
578:
577:
572:
570:
567:
557:
556:
539:
526:
522:
500:
498:
497:
492:
480:
478:
477:
472:
440:
438:
437:
432:
420:
418:
417:
412:
400:
398:
397:
392:
380:
378:
377:
372:
360:
358:
357:
352:
340:
338:
337:
332:
320:
318:
317:
312:
239:
237:
236:
231:
213:
211:
210:
205:
189:
187:
186:
181:
163:
161:
160:
155:
143:
141:
140:
135:
120:
118:
117:
112:
21:
8225:
8224:
8220:
8219:
8218:
8216:
8215:
8214:
8190:
8189:
8188:
8183:
8137:
8047:
8024:
7989:
7963:Data structures
7958:
7922:
7852:
7843:Program slicing
7802:
7701:
7672:Lambda calculus
7658:
7604:
7595:
7556:Hyperproperties
7534:
7529:
7465:
7442:
7440:Further reading
7437:
7402:
7398:
7391:
7375:
7371:
7366:
7362:
7347:
7340:
7328:
7324:
7301:(10): 576–580.
7285:Hoare, C. A. R.
7282:
7275:
7271:
7266:
7265:
7258:
7254:
7250:
7246:
7242:
7238:
7199:
7198:
7183:
7182:
7167:
7166:
7156:
7077:
7074:
7072:
7069:
7068:
7066:
7062:
7038:
7034:
7032:
7029:
7028:
7024:
7020:
7016:
7012:
7008:
7004:
6976:
6973:
6971:
6968:
6967:
6961:
6957:
6920:
6917:
6916:
6915:" rather than "
6888:
6885:
6884:
6882:
6878:
6873:
6868:
6824:
6815:
6761:
6758:
6757:
6699:
6696:
6695:
6587:
6584:
6583:
6482:
6479:
6478:
6450:
6447:
6446:
6301:
6298:
6297:
6272:
6269:
6268:
6264:
6260:
6210:
6209:
6182:
6181:
6160:
6159:
6142:
6139:
6138:
6124:
6120:
6116:
6113:minimal element
6108:
6104:
6100:
6080:
6075:
6074:
6072:
6069:
6068:
6049:
6047:
6044:
6043:
6027:
6025:
6022:
6021:
6014:
6010:
6006:
5998:
5994:
5990:
5979:
5921:
5920:
5905:
5904:
5889:
5888:
5866:
5774:
5767:
5764:
5762:
5759:
5758:
5744:
5731:
5727:
5696:
5695:
5686:
5685:
5658:
5657:
5652:
5649:
5648:
5641:
5637:
5614:
5613:
5586:
5585:
5576:
5575:
5566:
5565:
5538:
5537:
5528:
5527:
5522:
5519:
5518:
5511:
5507:
5503:
5499:
5468:
5465:
5464:
5421:
5418:
5417:
5355:
5352:
5351:
5279:
5276:
5275:
5222:
5221:
5194:
5193:
5172:
5171:
5154:
5151:
5150:
5140:
5121:
5118:
5117:
5113:
5109:
5101:
5059:
5058:
5043:
5042:
5027:
5026:
5016:
4987:
4984:
4982:
4979:
4978:
4975:
4966:
4962:
4934:
4931:
4930:
4910:
4909:
4904:
4901:
4900:
4872:
4869:
4868:
4851:
4847:
4845:
4842:
4841:
4824:
4820:
4818:
4815:
4814:
4760:
4759:
4754:
4751:
4750:
4684:
4681:
4680:
4673:
4636:
4633:
4632:
4595:
4592:
4591:
4514:
4511:
4510:
4432:
4429:
4428:
4397:
4394:
4393:
4389:
4385:
4378:
4317:
4314:
4313:
4235:
4232:
4231:
4224:
4151:
4148:
4147:
4063:
4060:
4059:
4015:
4014:
3993:
3992:
3965:
3964:
3943:
3942:
3919:
3916:
3915:
3905:
3901:
3884:
3880:
3878:
3875:
3874:
3857:
3853:
3851:
3848:
3847:
3820:
3816:
3801:
3797:
3793:
3786:
3782:
3773:
3769:
3755:
3751:
3736:
3732:
3718:
3714:
3705:
3701:
3700:
3697:
3695:
3692:
3691:
3688:
3675:
3671:
3667:
3663:
3659:
3639:
3638:
3629:
3628:
3607:
3606:
3582:
3581:
3572:
3571:
3556:
3555:
3546:
3545:
3524:
3523:
3502:
3501:
3492:
3491:
3476:
3475:
3473:
3470:
3469:
3446:
3445:
3430:
3429:
3414:
3413:
3398:
3397:
3395:
3392:
3391:
3377:
3373:
3369:
3365:
3361:
3357:
3353:
3349:
3345:
3312:
3311:
3296:
3295:
3280:
3279:
3264:
3263:
3253:
3189:
3186:
3184:
3181:
3180:
3177:
3093:
3090:
3089:
3031:
3028:
3027:
2957:
2954:
2953:
2904:
2855:
2852:
2850:
2847:
2846:
2835:
2813:
2810:
2809:
2808:and is written
2805:
2801:
2797:
2793:
2744:
2741:
2740:
2702:
2699:
2698:
2644:
2641:
2640:
2599:
2596:
2595:
2541:
2538:
2537:
2495:
2492:
2491:
2443:
2440:
2439:
2376:
2373:
2372:
2332:
2329:
2328:
2306:
2303:
2302:
2298:
2294:
2290:
2286:
2282:
2278:
2274:
2265:
2259:
2226:
2223:
2222:
2197:
2183:
2180:
2179:
2157:
2154:
2153:
2145:
2141:
2086:
2083:
2082:
1961:
1958:
1957:
1855:
1852:
1851:
1749:
1746:
1745:
1649:
1646:
1645:
1618:
1607:
1604:
1603:
1599:
1520:
1517:
1516:
1461:
1458:
1457:
1398:
1395:
1394:
1366:
1334:
1331:
1330:
1294:
1291:
1290:
1262:
1259:
1258:
1230:
1227:
1226:
1204:
1181:
1178:
1177:
1149:
1146:
1145:
1123:
1120:
1119:
1115:
1087:
1084:
1083:
1055:
1052:
1051:
982:
979:
978:
913:
910:
909:
897:
875:
861:
858:
857:
835:
824:
821:
820:
816:
794:
783:
780:
779:
775:
753:
742:
739:
738:
731:
723:
720:free occurrence
715:
693:
682:
679:
678:
628:
615:
611:
609:
606:
605:
594:
590:
587:
552:
551:
541:
537:
535:
532:
531:
524:
520:
517:empty statement
513:
508:
486:
483:
482:
454:
451:
450:
426:
423:
422:
406:
403:
402:
386:
383:
382:
366:
363:
362:
346:
343:
342:
326:
323:
322:
306:
303:
302:
293:can be proven.
287:
259:inference rules
248:predicate logic
225:
222:
221:
199:
196:
195:
175:
172:
171:
149:
146:
145:
129:
126:
125:
88:
85:
84:
70:
58:Robert W. Floyd
33:(also known as
28:
23:
22:
15:
12:
11:
5:
8223:
8213:
8212:
8207:
8202:
8185:
8184:
8182:
8181:
8171:
8161:
8150:
8147:
8146:
8143:
8142:
8139:
8138:
8136:
8135:
8130:
8125:
8120:
8115:
8110:
8105:
8104:
8103:
8093:
8088:
8083:
8078:
8073:
8068:
8063:
8057:
8055:
8049:
8048:
8046:
8045:
8040:
8034:
8032:
8026:
8025:
8023:
8022:
8017:
8012:
8006:
8004:
7995:
7991:
7990:
7988:
7987:
7982:
7977:
7972:
7966:
7964:
7960:
7959:
7957:
7956:
7951:
7946:
7941:
7936:
7930:
7928:
7924:
7923:
7921:
7920:
7915:
7914:
7913:
7903:
7894:
7889:
7884:
7882:Loop invariant
7879:
7873:
7871:
7864:
7862:Formal methods
7858:
7857:
7854:
7853:
7851:
7850:
7845:
7840:
7835:
7830:
7825:
7824:
7823:
7821:Taint tracking
7812:
7810:
7804:
7803:
7801:
7800:
7795:
7790:
7785:
7780:
7775:
7770:
7768:Model checking
7765:
7760:
7755:
7750:
7745:
7744:
7743:
7733:
7728:
7722:
7720:
7711:
7707:
7706:
7703:
7702:
7700:
7699:
7697:Turing machine
7694:
7689:
7684:
7679:
7674:
7668:
7666:
7660:
7659:
7657:
7656:
7655:
7654:
7649:
7639:
7638:
7637:
7627:
7621:
7619:
7612:
7606:
7605:
7598:
7596:
7594:
7593:
7588:
7583:
7578:
7576:Rice's theorem
7573:
7568:
7566:Path explosion
7563:
7558:
7553:
7548:
7542:
7540:
7536:
7535:
7528:
7527:
7520:
7513:
7505:
7499:
7498:
7476:
7464:
7463:External links
7461:
7460:
7459:
7441:
7438:
7436:
7435:
7396:
7390:978-0521543101
7389:
7369:
7360:
7338:
7322:
7272:
7270:
7267:
7264:
7263:
7222:
7219:
7216:
7213:
7210:
7207:
7194:
7178:
7165:
7162:
7159:
7154:
7151:
7148:
7145:
7142:
7139:
7136:
7133:
7130:
7127:
7124:
7121:
7118:
7115:
7112:
7109:
7106:
7102:
7098:
7095:
7092:
7089:
7086:
7083:
7080:
7060:
7042:
6989:
6985:
6982:
6979:
6955:
6942:
6939:
6936:
6933:
6930:
6927:
6924:
6904:
6901:
6898:
6895:
6892:
6875:
6874:
6872:
6869:
6867:
6866:
6861:
6856:
6854:Loop invariant
6851:
6846:
6841:
6836:
6831:
6825:
6823:
6820:
6808:
6807:
6795:
6792:
6789:
6786:
6783:
6780:
6777:
6774:
6771:
6768:
6765:
6745:
6742:
6739:
6736:
6733:
6730:
6727:
6724:
6721:
6718:
6715:
6712:
6709:
6706:
6703:
6693:
6681:
6678:
6675:
6672:
6669:
6666:
6663:
6660:
6657:
6654:
6651:
6648:
6645:
6642:
6639:
6636:
6633:
6630:
6627:
6624:
6621:
6618:
6615:
6612:
6609:
6606:
6603:
6600:
6597:
6594:
6591:
6577:
6576:
6564:
6561:
6558:
6555:
6552:
6549:
6546:
6543:
6540:
6537:
6534:
6531:
6528:
6525:
6522:
6519:
6516:
6513:
6510:
6507:
6504:
6501:
6498:
6495:
6492:
6489:
6486:
6460:
6457:
6454:
6443:
6442:
6431:
6428:
6425:
6422:
6419:
6416:
6413:
6410:
6407:
6404:
6401:
6398:
6395:
6392:
6389:
6386:
6383:
6380:
6377:
6374:
6371:
6368:
6365:
6362:
6359:
6356:
6353:
6350:
6347:
6344:
6341:
6338:
6335:
6332:
6329:
6326:
6323:
6320:
6317:
6314:
6311:
6308:
6305:
6282:
6279:
6276:
6257:
6256:
6245:
6242:
6239:
6236:
6233:
6230:
6227:
6224:
6221:
6218:
6205:
6202:
6199:
6196:
6193:
6177:
6174:
6171:
6158:
6155:
6152:
6149:
6146:
6083:
6078:
6052:
6030:
6005:of members of
5972:
5971:
5956:
5953:
5950:
5947:
5944:
5941:
5938:
5935:
5932:
5929:
5916:
5900:
5887:
5884:
5881:
5878:
5875:
5872:
5869:
5864:
5861:
5858:
5855:
5852:
5849:
5846:
5843:
5840:
5837:
5834:
5831:
5828:
5825:
5822:
5819:
5816:
5813:
5810:
5807:
5804:
5801:
5798:
5795:
5792:
5788:
5784:
5770:
5743:
5740:
5717:
5716:
5704:
5694:
5684:
5681:
5678:
5675:
5672:
5669:
5666:
5656:
5634:
5633:
5622:
5612:
5609:
5606:
5603:
5600:
5597:
5594:
5561:
5558:
5555:
5552:
5549:
5536:
5526:
5484:
5481:
5478:
5475:
5472:
5452:
5449:
5446:
5443:
5440:
5437:
5434:
5431:
5428:
5425:
5414:
5413:
5401:
5398:
5395:
5392:
5389:
5386:
5383:
5380:
5377:
5374:
5371:
5368:
5365:
5362:
5359:
5349:
5337:
5334:
5331:
5328:
5325:
5322:
5319:
5316:
5313:
5310:
5307:
5304:
5301:
5298:
5295:
5292:
5289:
5286:
5283:
5269:
5268:
5257:
5254:
5251:
5248:
5245:
5242:
5239:
5236:
5233:
5230:
5217:
5214:
5211:
5208:
5205:
5189:
5186:
5183:
5170:
5167:
5164:
5161:
5158:
5128:
5125:
5106:loop invariant
5098:
5097:
5082:
5079:
5076:
5073:
5070:
5067:
5054:
5038:
5025:
5022:
5019:
5014:
5011:
5008:
5005:
5002:
4999:
4996:
4993:
4990:
4974:
4971:
4950:
4947:
4944:
4941:
4938:
4918:
4908:
4888:
4885:
4882:
4879:
4876:
4854:
4850:
4827:
4823:
4811:
4810:
4798:
4795:
4792:
4789:
4786:
4783:
4780:
4777:
4774:
4771:
4768:
4758:
4748:
4736:
4733:
4730:
4727:
4724:
4721:
4718:
4715:
4712:
4709:
4706:
4703:
4700:
4697:
4694:
4691:
4688:
4658:
4655:
4652:
4649:
4646:
4643:
4640:
4620:
4617:
4614:
4611:
4608:
4605:
4602:
4599:
4588:
4587:
4575:
4572:
4569:
4566:
4563:
4560:
4557:
4554:
4551:
4548:
4545:
4542:
4539:
4536:
4533:
4530:
4527:
4524:
4521:
4518:
4508:
4496:
4493:
4490:
4487:
4484:
4481:
4478:
4475:
4472:
4469:
4466:
4463:
4460:
4457:
4454:
4451:
4448:
4445:
4442:
4439:
4436:
4413:
4410:
4407:
4404:
4401:
4375:
4374:
4363:
4360:
4357:
4354:
4351:
4348:
4345:
4342:
4339:
4336:
4333:
4330:
4327:
4324:
4321:
4311:
4299:
4296:
4293:
4290:
4287:
4284:
4281:
4278:
4275:
4272:
4269:
4266:
4263:
4260:
4257:
4254:
4251:
4248:
4245:
4242:
4239:
4221:
4220:
4209:
4206:
4203:
4200:
4197:
4194:
4191:
4188:
4185:
4182:
4179:
4176:
4173:
4170:
4167:
4164:
4161:
4158:
4155:
4145:
4133:
4130:
4127:
4124:
4121:
4118:
4115:
4112:
4109:
4106:
4103:
4100:
4097:
4094:
4091:
4088:
4085:
4082:
4079:
4076:
4073:
4070:
4067:
4053:
4052:
4041:
4038:
4035:
4032:
4029:
4026:
4023:
4010:
4007:
4004:
3988:
3985:
3982:
3979:
3976:
3960:
3957:
3954:
3941:
3938:
3935:
3932:
3929:
3926:
3923:
3887:
3883:
3860:
3856:
3844:
3843:
3828:
3823:
3819:
3815:
3812:
3809:
3804:
3800:
3796:
3789:
3785:
3781:
3776:
3772:
3767:
3763:
3758:
3754:
3750:
3747:
3744:
3739:
3735:
3731:
3727:
3721:
3717:
3713:
3708:
3704:
3687:
3684:
3656:
3655:
3627:
3624:
3621:
3618:
3602:
3599:
3596:
3593:
3580:
3570:
3567:
3564:
3544:
3541:
3538:
3535:
3519:
3516:
3513:
3500:
3490:
3487:
3463:
3462:
3441:
3425:
3409:
3342:
3341:
3326:
3323:
3320:
3307:
3291:
3275:
3262:
3259:
3256:
3251:
3248:
3245:
3242:
3239:
3236:
3233:
3230:
3227:
3224:
3220:
3216:
3213:
3210:
3207:
3204:
3201:
3198:
3195:
3192:
3176:
3173:
3169:
3168:
3157:
3154:
3151:
3148:
3145:
3142:
3139:
3136:
3133:
3130:
3127:
3124:
3121:
3118:
3115:
3112:
3109:
3106:
3103:
3100:
3097:
3083:
3082:
3071:
3068:
3065:
3062:
3059:
3056:
3053:
3050:
3047:
3044:
3041:
3038:
3035:
3021:
3020:
3009:
3006:
3003:
3000:
2997:
2994:
2991:
2988:
2985:
2982:
2979:
2976:
2973:
2970:
2967:
2964:
2961:
2947:
2946:
2931:
2928:
2925:
2922:
2919:
2916:
2913:
2910:
2907:
2902:
2899:
2896:
2893:
2890:
2887:
2884:
2880:
2876:
2873:
2870:
2867:
2864:
2861:
2858:
2838:is called the
2823:
2820:
2817:
2788:
2787:
2784:
2783:
2772:
2769:
2766:
2763:
2760:
2757:
2754:
2751:
2748:
2738:
2736:
2730:
2729:
2718:
2715:
2712:
2709:
2706:
2696:
2690:
2689:
2678:
2675:
2672:
2669:
2666:
2663:
2660:
2657:
2654:
2651:
2648:
2638:
2636:
2630:
2629:
2618:
2615:
2612:
2609:
2606:
2603:
2593:
2587:
2586:
2575:
2572:
2569:
2566:
2563:
2560:
2557:
2554:
2551:
2548:
2545:
2535:
2533:
2527:
2526:
2514:
2511:
2508:
2505:
2502:
2499:
2489:
2483:
2482:
2471:
2468:
2465:
2462:
2459:
2456:
2453:
2450:
2447:
2437:
2435:
2428:
2427:
2422:
2417:
2398:
2395:
2392:
2389:
2386:
2383:
2380:
2360:
2357:
2354:
2351:
2348:
2345:
2342:
2339:
2336:
2316:
2313:
2310:
2268:
2267:
2258:
2255:
2242:
2239:
2236:
2233:
2230:
2210:
2207:
2204:
2200:
2196:
2193:
2190:
2187:
2167:
2164:
2161:
2138:
2137:
2126:
2123:
2120:
2117:
2114:
2111:
2108:
2105:
2102:
2099:
2096:
2093:
2090:
2076:does not apply
2069:
2068:
2067:
2066:
2055:
2052:
2049:
2046:
2043:
2040:
2037:
2034:
2031:
2028:
2025:
2022:
2019:
2016:
2013:
2010:
2007:
2004:
2001:
1998:
1995:
1992:
1989:
1986:
1983:
1980:
1977:
1974:
1971:
1968:
1965:
1955:
1943:
1940:
1937:
1934:
1931:
1928:
1925:
1922:
1919:
1916:
1913:
1910:
1907:
1904:
1901:
1898:
1895:
1892:
1889:
1886:
1883:
1880:
1877:
1874:
1871:
1868:
1865:
1862:
1859:
1849:
1837:
1834:
1831:
1828:
1825:
1822:
1819:
1816:
1813:
1810:
1807:
1804:
1801:
1798:
1795:
1792:
1789:
1786:
1783:
1780:
1777:
1774:
1771:
1768:
1765:
1762:
1759:
1756:
1753:
1743:
1731:
1728:
1725:
1722:
1719:
1716:
1713:
1710:
1707:
1704:
1701:
1698:
1695:
1692:
1689:
1686:
1683:
1680:
1677:
1674:
1671:
1668:
1665:
1662:
1659:
1656:
1653:
1628:
1625:
1621:
1617:
1614:
1611:
1596:
1595:
1584:
1581:
1578:
1575:
1572:
1569:
1566:
1563:
1560:
1557:
1554:
1551:
1548:
1545:
1542:
1539:
1536:
1533:
1530:
1527:
1524:
1501:
1498:
1495:
1492:
1489:
1486:
1483:
1480:
1477:
1474:
1471:
1468:
1465:
1450:
1449:
1438:
1435:
1432:
1429:
1426:
1423:
1420:
1417:
1414:
1411:
1408:
1405:
1402:
1379:
1376:
1373:
1369:
1365:
1362:
1359:
1356:
1353:
1350:
1347:
1344:
1341:
1338:
1310:
1307:
1304:
1301:
1298:
1278:
1275:
1272:
1269:
1266:
1246:
1243:
1240:
1237:
1234:
1214:
1211:
1207:
1203:
1200:
1197:
1194:
1191:
1188:
1185:
1165:
1162:
1159:
1156:
1153:
1133:
1130:
1127:
1103:
1100:
1097:
1094:
1091:
1071:
1068:
1065:
1062:
1059:
1048:
1047:
1046:
1045:
1034:
1031:
1028:
1025:
1022:
1019:
1016:
1013:
1010:
1007:
1004:
1001:
998:
995:
992:
989:
986:
976:
965:
962:
959:
956:
953:
950:
947:
944:
941:
938:
935:
932:
929:
926:
923:
920:
917:
885:
882:
878:
874:
871:
868:
865:
845:
842:
838:
834:
831:
828:
804:
801:
797:
793:
790:
787:
763:
760:
756:
752:
749:
746:
718:in which each
703:
700:
696:
692:
689:
686:
675:
674:
659:
656:
653:
650:
647:
644:
641:
638:
635:
631:
627:
624:
621:
618:
586:
583:
582:
581:
566:
563:
560:
550:
547:
544:
512:
509:
507:
504:
490:
470:
467:
464:
461:
458:
430:
410:
390:
370:
350:
330:
310:
286:
283:
229:
203:
179:
153:
133:
122:
121:
110:
107:
104:
101:
98:
95:
92:
69:
66:
26:
9:
6:
4:
3:
2:
8222:
8211:
8208:
8206:
8205:Program logic
8203:
8201:
8198:
8197:
8195:
8180:
8172:
8170:
8162:
8160:
8152:
8151:
8148:
8134:
8131:
8129:
8126:
8124:
8121:
8119:
8116:
8114:
8111:
8109:
8106:
8102:
8099:
8098:
8097:
8094:
8092:
8089:
8087:
8084:
8082:
8079:
8077:
8074:
8072:
8069:
8067:
8064:
8062:
8059:
8058:
8056:
8054:
8050:
8044:
8041:
8039:
8036:
8035:
8033:
8031:
8027:
8021:
8018:
8016:
8013:
8011:
8008:
8007:
8005:
8003:
7999:
7996:
7992:
7986:
7983:
7981:
7978:
7976:
7973:
7971:
7968:
7967:
7965:
7961:
7955:
7952:
7950:
7947:
7945:
7942:
7940:
7939:Incorrectness
7937:
7935:
7932:
7931:
7929:
7925:
7919:
7916:
7912:
7909:
7908:
7907:
7906:Specification
7904:
7902:
7898:
7895:
7893:
7890:
7888:
7885:
7883:
7880:
7878:
7875:
7874:
7872:
7868:
7865:
7863:
7859:
7849:
7846:
7844:
7841:
7839:
7836:
7834:
7831:
7829:
7826:
7822:
7819:
7818:
7817:
7814:
7813:
7811:
7809:
7805:
7799:
7796:
7794:
7791:
7789:
7786:
7784:
7781:
7779:
7776:
7774:
7771:
7769:
7766:
7764:
7761:
7759:
7758:Effect system
7756:
7754:
7751:
7749:
7746:
7742:
7739:
7738:
7737:
7734:
7732:
7729:
7727:
7724:
7723:
7721:
7719:
7715:
7712:
7708:
7698:
7695:
7693:
7692:State machine
7690:
7688:
7685:
7683:
7680:
7678:
7675:
7673:
7670:
7669:
7667:
7665:
7661:
7653:
7650:
7648:
7645:
7644:
7643:
7640:
7636:
7633:
7632:
7631:
7628:
7626:
7623:
7622:
7620:
7616:
7613:
7611:
7607:
7602:
7592:
7589:
7587:
7584:
7582:
7579:
7577:
7574:
7572:
7569:
7567:
7564:
7562:
7559:
7557:
7554:
7552:
7549:
7547:
7544:
7543:
7541:
7537:
7533:
7526:
7521:
7519:
7514:
7512:
7507:
7506:
7503:
7496:
7492:
7488:
7484:
7480:
7477:
7474:
7470:
7467:
7466:
7458:
7457:0-521-00401-2
7454:
7450:
7449:
7444:
7443:
7431:
7427:
7423:
7419:
7415:
7411:
7407:
7400:
7392:
7386:
7382:
7381:
7373:
7364:
7355:
7351:
7345:
7343:
7335:
7331:
7326:
7318:
7314:
7309:
7304:
7300:
7296:
7295:
7290:
7286:
7280:
7278:
7273:
7217:
7211:
7208:
7192:
7176:
7160:
7149:
7146:
7143:
7140:
7137:
7131:
7125:
7122:
7119:
7116:
7113:
7110:
7107:
7100:
7096:
7093:
7090:
7084:
7081:
7078:
7064:
7040:
6987:
6983:
6980:
6977:
6965:
6959:
6937:
6931:
6925:
6902:
6896:
6890:
6880:
6876:
6865:
6862:
6860:
6857:
6855:
6852:
6850:
6847:
6845:
6844:Dynamic logic
6842:
6840:
6837:
6835:
6832:
6830:
6827:
6826:
6819:
6813:
6790:
6787:
6784:
6781:
6778:
6775:
6772:
6769:
6766:
6740:
6737:
6734:
6731:
6728:
6725:
6722:
6719:
6716:
6713:
6710:
6707:
6704:
6694:
6676:
6673:
6670:
6667:
6664:
6661:
6658:
6655:
6652:
6646:
6643:
6640:
6637:
6634:
6628:
6625:
6622:
6619:
6616:
6613:
6610:
6607:
6604:
6601:
6598:
6595:
6592:
6582:
6581:
6580:
6559:
6556:
6553:
6550:
6547:
6544:
6541:
6538:
6535:
6529:
6526:
6523:
6520:
6517:
6511:
6508:
6505:
6502:
6499:
6496:
6493:
6490:
6487:
6477:
6476:
6475:
6472:
6458:
6455:
6452:
6426:
6423:
6420:
6417:
6414:
6411:
6408:
6405:
6402:
6399:
6396:
6393:
6390:
6387:
6384:
6378:
6375:
6372:
6369:
6366:
6360:
6357:
6354:
6351:
6348:
6345:
6342:
6339:
6336:
6333:
6330:
6327:
6324:
6321:
6318:
6315:
6312:
6309:
6306:
6296:
6295:
6294:
6280:
6277:
6274:
6240:
6237:
6234:
6231:
6228:
6225:
6222:
6203:
6200:
6197:
6194:
6191:
6175:
6172:
6169:
6153:
6150:
6147:
6137:
6136:
6135:
6133:
6128:
6114:
6097:
6081:
6067:
6020:
6004:
5989:
5985:
5982:, called the
5977:
5951:
5948:
5945:
5942:
5939:
5936:
5933:
5914:
5898:
5882:
5879:
5876:
5873:
5870:
5859:
5856:
5853:
5850:
5847:
5844:
5841:
5838:
5835:
5829:
5823:
5820:
5817:
5814:
5811:
5808:
5805:
5802:
5799:
5796:
5793:
5786:
5782:
5768:
5757:
5756:
5755:
5753:
5749:
5739:
5737:
5725:
5720:
5679:
5676:
5673:
5670:
5667:
5664:
5647:
5646:
5645:
5610:
5607:
5604:
5601:
5598:
5595:
5559:
5556:
5553:
5550:
5547:
5517:
5516:
5515:
5496:
5479:
5476:
5473:
5447:
5444:
5441:
5438:
5435:
5432:
5429:
5396:
5393:
5390:
5384:
5381:
5378:
5375:
5372:
5366:
5363:
5360:
5350:
5332:
5329:
5326:
5320:
5317:
5314:
5311:
5308:
5302:
5299:
5296:
5293:
5290:
5287:
5284:
5274:
5273:
5272:
5252:
5249:
5246:
5243:
5240:
5237:
5234:
5215:
5212:
5209:
5206:
5203:
5187:
5184:
5181:
5165:
5162:
5159:
5149:
5148:
5147:
5144:
5126:
5107:
5077:
5074:
5071:
5052:
5036:
5020:
5009:
5003:
4997:
4994:
4991:
4977:
4976:
4970:
4945:
4942:
4939:
4883:
4880:
4877:
4852:
4848:
4825:
4821:
4793:
4790:
4787:
4784:
4781:
4775:
4772:
4769:
4749:
4731:
4728:
4725:
4722:
4719:
4713:
4710:
4707:
4701:
4698:
4695:
4692:
4689:
4679:
4678:
4677:
4670:
4653:
4650:
4647:
4644:
4641:
4615:
4612:
4609:
4606:
4603:
4600:
4570:
4567:
4564:
4561:
4558:
4552:
4549:
4546:
4543:
4540:
4534:
4531:
4528:
4525:
4522:
4519:
4509:
4491:
4488:
4485:
4482:
4479:
4473:
4470:
4467:
4464:
4461:
4455:
4452:
4449:
4446:
4443:
4440:
4437:
4427:
4426:
4425:
4411:
4408:
4405:
4402:
4399:
4382:
4358:
4355:
4352:
4349:
4346:
4340:
4337:
4334:
4328:
4325:
4322:
4312:
4294:
4291:
4288:
4285:
4282:
4276:
4273:
4270:
4264:
4261:
4258:
4255:
4252:
4249:
4246:
4243:
4240:
4230:
4229:
4228:
4204:
4201:
4198:
4195:
4192:
4186:
4183:
4180:
4177:
4174:
4168:
4165:
4162:
4159:
4156:
4146:
4128:
4125:
4122:
4119:
4116:
4110:
4107:
4104:
4101:
4098:
4092:
4089:
4086:
4083:
4080:
4077:
4074:
4071:
4068:
4058:
4057:
4056:
4036:
4033:
4030:
4027:
4024:
4008:
4005:
4002:
3986:
3983:
3980:
3977:
3974:
3958:
3955:
3952:
3936:
3933:
3930:
3927:
3924:
3914:
3913:
3912:
3909:
3885:
3881:
3858:
3854:
3821:
3817:
3810:
3802:
3798:
3787:
3783:
3774:
3770:
3765:
3756:
3752:
3745:
3737:
3733:
3725:
3719:
3715:
3706:
3702:
3690:
3689:
3683:
3681:
3625:
3622:
3619:
3616:
3600:
3597:
3594:
3578:
3568:
3565:
3562:
3542:
3539:
3536:
3533:
3517:
3514:
3511:
3498:
3488:
3485:
3468:
3467:
3466:
3439:
3423:
3407:
3390:
3389:
3388:
3385:
3383:
3321:
3305:
3289:
3273:
3257:
3246:
3240:
3234:
3231:
3228:
3218:
3211:
3205:
3199:
3196:
3193:
3179:
3178:
3172:
3152:
3149:
3146:
3140:
3137:
3134:
3131:
3128:
3125:
3122:
3119:
3116:
3110:
3107:
3104:
3101:
3098:
3088:
3087:
3086:
3066:
3063:
3060:
3054:
3051:
3048:
3042:
3039:
3036:
3026:
3025:
3024:
3004:
3001:
2998:
2992:
2989:
2986:
2983:
2980:
2974:
2971:
2968:
2965:
2962:
2952:
2951:
2950:
2926:
2920:
2917:
2914:
2908:
2897:
2891:
2885:
2878:
2871:
2865:
2859:
2845:
2844:
2843:
2841:
2821:
2818:
2815:
2767:
2764:
2761:
2758:
2755:
2752:
2749:
2739:
2737:
2735:
2732:
2731:
2716:
2713:
2710:
2707:
2704:
2697:
2695:
2692:
2691:
2673:
2670:
2667:
2664:
2661:
2658:
2655:
2652:
2649:
2639:
2637:
2635:
2632:
2631:
2616:
2613:
2610:
2607:
2604:
2601:
2594:
2592:
2589:
2588:
2570:
2567:
2564:
2561:
2558:
2555:
2552:
2549:
2546:
2536:
2534:
2532:
2529:
2528:
2512:
2509:
2506:
2503:
2500:
2497:
2490:
2488:
2485:
2484:
2466:
2463:
2460:
2457:
2454:
2451:
2448:
2438:
2436:
2433:
2430:
2429:
2426:
2421:
2418:
2416:
2413:
2412:
2396:
2393:
2390:
2387:
2384:
2381:
2378:
2358:
2355:
2349:
2346:
2343:
2337:
2334:
2314:
2311:
2308:
2270:
2269:
2263:
2262:
2254:
2237:
2234:
2231:
2202:
2198:
2194:
2188:
2162:
2151:
2121:
2118:
2115:
2109:
2106:
2103:
2097:
2094:
2091:
2081:
2080:
2079:
2077:
2072:
2050:
2047:
2044:
2041:
2038:
2035:
2032:
2029:
2026:
2023:
2020:
2014:
2011:
2008:
2005:
2002:
1996:
1993:
1990:
1987:
1984:
1981:
1978:
1975:
1972:
1969:
1966:
1956:
1938:
1935:
1932:
1929:
1926:
1923:
1920:
1917:
1914:
1908:
1905:
1902:
1899:
1896:
1890:
1887:
1884:
1881:
1878:
1875:
1872:
1869:
1866:
1863:
1860:
1850:
1832:
1829:
1826:
1823:
1820:
1817:
1814:
1811:
1808:
1802:
1799:
1796:
1793:
1790:
1784:
1781:
1778:
1775:
1772:
1769:
1766:
1763:
1760:
1757:
1754:
1744:
1726:
1723:
1720:
1717:
1714:
1711:
1708:
1702:
1699:
1696:
1693:
1690:
1684:
1681:
1678:
1675:
1672:
1669:
1666:
1663:
1660:
1657:
1654:
1644:
1643:
1642:
1641:
1640:
1623:
1619:
1615:
1609:
1579:
1576:
1573:
1570:
1567:
1564:
1561:
1558:
1555:
1549:
1546:
1543:
1540:
1537:
1531:
1528:
1525:
1515:
1514:
1513:
1496:
1493:
1490:
1487:
1484:
1478:
1475:
1472:
1466:
1455:
1433:
1430:
1427:
1421:
1418:
1415:
1409:
1406:
1403:
1393:
1392:
1391:
1371:
1367:
1363:
1357:
1351:
1348:
1345:
1339:
1328:
1322:
1308:
1305:
1302:
1299:
1296:
1276:
1273:
1270:
1267:
1264:
1244:
1241:
1238:
1235:
1232:
1209:
1205:
1198:
1195:
1192:
1183:
1163:
1160:
1157:
1154:
1151:
1131:
1128:
1125:
1101:
1098:
1095:
1092:
1089:
1069:
1066:
1063:
1060:
1057:
1029:
1026:
1023:
1017:
1014:
1011:
1008:
1005:
999:
996:
993:
990:
987:
977:
960:
957:
954:
948:
945:
942:
939:
936:
930:
927:
924:
921:
918:
908:
907:
906:
905:
904:
901:
880:
876:
872:
866:
840:
836:
832:
826:
799:
795:
791:
785:
758:
754:
750:
744:
735:
729:
721:
698:
694:
690:
684:
654:
648:
645:
642:
633:
629:
625:
619:
604:
603:
602:
600:
561:
545:
530:
529:
528:
518:
502:
488:
468:
462:
456:
445:
442:
428:
408:
388:
368:
348:
328:
308:
300:
296:
292:
282:
280:
276:
272:
268:
264:
260:
256:
251:
249:
245:
244:
243:postcondition
227:
219:
218:
214:is named the
201:
193:
177:
169:
168:
151:
131:
105:
99:
93:
83:
82:
81:
79:
75:
65:
63:
59:
55:
52:
48:
44:
43:formal system
40:
36:
32:
19:
8101:Isabelle/HOL
7933:
7918:Verification
7901:completeness
7793:Type systems
7736:Control flow
7630:Denotational
7571:Polyvariance
7539:Key concepts
7446:
7413:
7409:
7399:
7379:
7372:
7363:
7353:
7325:
7298:
7292:
7063:
6958:
6879:
6809:
6578:
6473:
6444:
6258:
6129:
6098:
5984:loop variant
5973:
5745:
5735:
5723:
5721:
5718:
5635:
5497:
5415:
5270:
5145:
5099:
4812:
4671:
4589:
4383:
4376:
4222:
4054:
3910:
3845:
3657:
3464:
3386:
3382:next section
3343:
3170:
3084:
3022:
2948:
2840:midcondition
2839:
2791:
2733:
2693:
2633:
2590:
2530:
2486:
2431:
2424:
2419:
2414:
2409:(line 3→1).
2140:is wrong if
2139:
2075:
2073:
2070:
1597:
1453:
1451:
1326:
1323:
1049:
902:
856:false (i.e.
778:. Thus were
736:
676:
588:
514:
447:
443:
288:
252:
241:
217:precondition
215:
191:
165:
123:
78:Hoare triple
77:
73:
71:
68:Hoare triple
38:
34:
30:
29:
18:Hoare triple
8030:Lightweight
7892:Side effect
7788:Termination
7642:Operational
7551:Correctness
7495:SourceForge
7330:R. W. Floyd
5976:termination
299:termination
267:concurrency
74:Hoare logic
39:Hoare rules
31:Hoare logic
8194:Categories
7985:Union-find
7949:Separation
7887:Refinement
7753:Dependence
7652:Small-step
7561:Invariants
7416:(6): 759.
7269:References
4973:While rule
4227:part, and
3664:do...until
3358:if...endif
3348:common to
2425:Assertions
271:procedures
167:assertions
62:flowcharts
54:Tony Hoare
8081:HOL Light
7911:Languages
7897:Soundness
7816:Data-flow
7798:Typestate
7748:Data-flow
7677:Petri net
7625:Axiomatic
7610:Semantics
7469:KeY-Hoare
7430:102351597
7317:207726175
7215:¬
7212:∧
7141:∧
7117:∧
7111:∧
7094:≤
7088:→
7082:∧
7041:ϕ
6988:ϕ
6984:β
6978:α
6782:−
6776:∧
6732:−
6726:−
6720:∧
6714:≤
6668:−
6662:∧
6656:≤
6620:−
6614:−
6608:∧
6602:≤
6551:−
6545:∧
6539:≤
6503:−
6497:∧
6456:−
6418:−
6412:∧
6406:≥
6400:−
6394:∧
6388:≤
6352:−
6346:∧
6340:≥
6334:−
6328:∧
6316:∧
6310:≤
6278:−
6238:≤
6232:∧
6220:¬
6151:≤
6111:is not a
5949:∈
5943:∧
5937:∧
5931:¬
5880:∈
5874:∧
5851:∧
5845:∈
5839:∧
5815:∧
5809:∈
5803:∧
5797:∧
5738:correct.
5724:partially
5677:≠
5671:⋅
5665:∧
5611:∧
5599:⋅
5557:≠
5551:⋅
5506:—even if
5445:≤
5439:∧
5427:¬
5394:≤
5330:≤
5294:∧
5288:≤
5250:≤
5244:∧
5232:¬
5163:≤
5124:¬
5075:∧
5069:¬
4995:∧
4791:≤
4785:≤
4729:≤
4723:≤
4699:≤
4693:≤
4645:≤
4607:≤
4601:−
4568:≤
4562:≤
4526:≤
4520:−
4489:≤
4483:≤
4453:≤
4441:≤
4409:≤
4403:≤
4356:≤
4350:≤
4292:≤
4286:≤
4262:≥
4256:∧
4250:≤
4244:≤
4202:≤
4196:≤
4160:≤
4126:≤
4120:≤
4084:∧
4078:≤
4072:≤
4034:≤
4028:≤
3934:≤
3928:≤
3780:→
3712:→
3598:∧
3592:¬
3515:∧
3232:∧
3226:¬
3197:∧
2759:∧
2714:−
2665:−
2659:∧
2611:−
2562:∧
2550:−
2458:∧
2388:−
2347:−
2338:−
2312:−
2048:≤
2042:⋅
2036:∧
2030:⋅
2024:≤
2012:⋅
1994:≤
1988:⋅
1982:∧
1976:⋅
1970:≤
1936:≤
1930:∧
1924:⋅
1918:≤
1906:⋅
1888:≤
1882:⋅
1876:∧
1870:⋅
1864:≤
1830:≤
1824:⋅
1818:∧
1812:≤
1800:⋅
1782:≤
1776:⋅
1770:∧
1764:⋅
1758:≤
1724:≤
1718:∧
1712:≤
1700:⋅
1682:≤
1676:⋅
1670:∧
1664:⋅
1658:≤
1565:∧
1488:∧
1454:incorrect
1327:incorrect
1027:≤
997:≤
864:¬
726:has been
8179:Glossary
8159:Category
8096:Isabelle
7980:Hashcons
7954:Temporal
7870:Concepts
7710:Analyses
7647:Big-step
7352:(2009).
7015:holds";
6822:See also
6019:integers
4377:for the
4223:for the
3904:and the
3676:continue
3364:and the
2800:, where
2150:aliasing
1452:Another
728:replaced
601:. Then:
279:pointers
51:logician
8169:Outline
7975:E-graph
7848:Testing
7833:Fuzzing
7808:Dynamic
7773:Pointer
6267:being
6064:nor on
5746:If the
5736:totally
5104:is the
1225:being (
1118:being (
341:, then
192:command
76:is the
41:) is a
7944:Linear
7927:Logics
7763:Escape
7718:Static
7664:Models
7491:j-Algo
7487:GitHub
7483:j-Algo
7455:
7428:
7387:
7315:
7257:, and
7196:
7190:
7180:
7174:
7025:φ
7021:β
7017:α
7013:φ
7009:β
7005:α
6207:
6189:
6179:
6167:
5918:
5912:
5902:
5896:
5780:
5772:
5640:being
5583:
5573:
5563:
5545:
5219:
5201:
5191:
5179:
5056:
5050:
5040:
5034:
4867:being
4381:part.
4012:
4000:
3990:
3972:
3962:
3950:
3908:part.
3668:switch
3666:loop,
3662:loop,
3636:
3614:
3604:
3589:
3553:
3531:
3521:
3509:
3483:
3443:
3437:
3427:
3421:
3411:
3405:
3309:
3303:
3293:
3287:
3277:
3271:
2221:being
677:where
277:, and
255:axioms
124:where
8133:Twelf
8123:NuPRL
8118:Mizar
8091:Idris
8038:Alloy
7994:Tools
7934:Hoare
7778:Shape
7731:Alias
7618:Types
7426:S2CID
7313:S2CID
7253:, or
7237:when
7169:while
6871:Notes
6162:while
6003:chain
5891:while
5540:while
5174:while
5100:Here
5029:while
4017:endif
3672:break
3631:false
3584:while
3548:false
3504:while
3448:endif
3314:endif
1954:, and
506:Rules
275:jumps
190:is a
8113:LEGO
8108:Lean
8086:HOL4
8066:Agda
8061:ACL2
8043:TLA+
7899:and
7741:kCFA
7453:ISBN
7385:ISBN
7201:done
7147:<
7019:and
7007:and
6770:<
6738:<
6674:<
6626:<
6557:<
6491:<
6424:<
6322:<
6226:<
6212:done
6173:<
6015:<
5999:<
5991:<
5923:done
5857:<
5769:<
5698:true
5688:skip
5660:true
5642:true
5616:true
5588:done
5578:skip
5530:true
5433:<
5364:<
5300:<
5238:<
5224:done
5185:<
5061:done
4967:else
4963:else
4912:true
4899:and
4840:and
4762:true
4674:else
4651:<
4613:<
4532:<
4386:then
4379:else
4225:then
4166:<
4090:<
3995:else
3967:then
3956:<
3906:else
3902:then
3641:done
3574:true
3558:done
3494:true
3478:bool
3432:else
3416:then
3366:else
3362:then
3354:else
3352:and
3350:then
3298:else
3282:then
3023:and
2796:and
2420:Code
2293:and
2285:and
2277:and
2178:and
2144:and
1257:and
1144:and
599:free
554:skip
525:skip
521:skip
515:The
257:and
240:the
220:and
170:and
164:are
144:and
8128:PVS
8071:Coq
8020:SMT
8015:SAT
8010:CHC
7970:BDD
7493:on
7485:on
7473:KeY
7418:doi
7332:. "
7303:doi
6115:of
4392:as
3660:for
2842:):
2253:).
722:of
597:is
37:or
8196::
8076:F*
7489:,
7424:.
7414:31
7412:.
7408:.
7341:^
7311:.
7299:12
7297:.
7291:.
7276:^
7249:,
7245:,
7185:do
6953:".
6779:10
6773:10
6723:10
6717:10
6665:10
6659:10
6638::=
6611:10
6605:10
6548:10
6542:10
6521::=
6500:10
6494:10
6453:10
6415:10
6397:10
6391:10
6370::=
6349:10
6331:10
6325:10
6313:10
6275:10
6241:10
6229:10
6195::=
6184:do
6176:10
6154:10
5907:do
5568:do
5495:.
5480:10
5448:10
5436:10
5397:10
5376::=
5367:10
5333:10
5312::=
5303:10
5291:10
5253:10
5241:10
5207::=
5196:do
5188:10
5166:10
5045:do
4946:15
4884:15
4794:15
4773::=
4732:15
4711::=
4702:15
4654:15
4616:15
4571:15
4544::=
4535:15
4492:15
4465::=
4456:15
4412:15
4359:15
4338::=
4329:15
4295:15
4274::=
4265:15
4253:15
4205:15
4178::=
4169:15
4129:15
4102::=
4093:15
4081:15
4037:15
4006::=
3978::=
3959:15
3945:if
3937:15
3674:,
3670:,
3626::=
3609:do
3569::=
3543::=
3526:do
3489::=
3400:if
3384:.
3266:if
3153:43
3138::=
3120::=
3111:43
3067:43
3052::=
3043:43
3005:43
2984::=
2975:43
2734:7:
2708::=
2694:6:
2634:5:
2605::=
2591:4:
2531:3:
2501::=
2487:2:
2432:1:
2415:Nr
2107::=
2006::=
1900::=
1794::=
1694::=
1541::=
1476::=
1419::=
1349::=
1321:.
1309:43
1277:43
1245:43
1164:43
1132:43
1102:43
1061::=
1009::=
961:43
940::=
931:43
734:.
646::=
281:.
273:,
269:,
250:.
194:.
64:.
7524:e
7517:t
7510:v
7481:(
7432:.
7420::
7393:.
7319:.
7305::
7259:t
7255:t
7251:S
7247:B
7243:P
7239:z
7221:]
7218:B
7209:P
7206:[
7193:S
7177:B
7164:]
7161:P
7158:[
7153:]
7150:z
7144:t
7138:P
7135:[
7132:S
7129:]
7126:z
7123:=
7120:t
7114:B
7108:P
7105:[
7101:,
7097:t
7091:0
7085:B
7079:P
7058:.
6981:,
6941:}
6938:Q
6935:{
6932:C
6929:}
6926:P
6923:{
6903:Q
6900:}
6897:C
6894:{
6891:P
6816:t
6794:]
6791:z
6788:=
6785:x
6767:x
6764:[
6744:]
6741:z
6735:1
6729:x
6711:1
6708:+
6705:x
6702:[
6680:]
6677:z
6671:x
6653:x
6650:[
6647:1
6644:+
6641:x
6635:x
6632:]
6629:z
6623:1
6617:x
6599:1
6596:+
6593:x
6590:[
6575:,
6563:]
6560:z
6554:x
6536:x
6533:[
6530:1
6527:+
6524:x
6518:x
6515:]
6512:z
6509:=
6506:x
6488:x
6485:[
6459:x
6430:]
6427:z
6421:x
6409:0
6403:x
6385:x
6382:[
6379:1
6376:+
6373:x
6367:x
6364:]
6361:z
6358:=
6355:x
6343:0
6337:x
6319:x
6307:x
6304:[
6281:x
6265:t
6261:D
6244:]
6235:x
6223:x
6217:[
6204:1
6201:+
6198:x
6192:x
6170:x
6157:]
6148:x
6145:[
6125:t
6121:S
6117:D
6109:t
6105:B
6101:P
6082:+
6077:R
6051:Z
6029:N
6011:t
6007:D
5995:D
5980:t
5955:]
5952:D
5946:t
5940:P
5934:B
5928:[
5915:S
5899:B
5886:]
5883:D
5877:t
5871:P
5868:[
5863:]
5860:z
5854:t
5848:D
5842:t
5836:P
5833:[
5830:S
5827:]
5824:z
5821:=
5818:t
5812:D
5806:t
5800:B
5794:P
5791:[
5787:,
5783:D
5732:a
5728:x
5715:,
5703:}
5693:{
5683:}
5680:a
5674:x
5668:x
5655:{
5638:P
5621:}
5608:a
5605:=
5602:x
5596:x
5593:{
5560:a
5554:x
5548:x
5535:}
5525:{
5512:a
5508:x
5504:a
5500:x
5483:}
5477:=
5474:x
5471:{
5451:}
5442:x
5430:x
5424:{
5412:,
5400:}
5391:x
5388:{
5385:1
5382:+
5379:x
5373:x
5370:}
5361:x
5358:{
5336:}
5327:x
5324:{
5321:1
5318:+
5315:x
5309:x
5306:}
5297:x
5285:x
5282:{
5256:}
5247:x
5235:x
5229:{
5216:1
5213:+
5210:x
5204:x
5182:x
5169:}
5160:x
5157:{
5141:B
5127:B
5114:P
5110:S
5102:P
5081:}
5078:P
5072:B
5066:{
5053:S
5037:B
5024:}
5021:P
5018:{
5013:}
5010:P
5007:{
5004:S
5001:}
4998:B
4992:P
4989:{
4949:}
4943:=
4940:x
4937:{
4917:}
4907:{
4887:}
4881:=
4878:x
4875:{
4853:2
4849:P
4826:1
4822:P
4809:,
4797:}
4788:x
4782:0
4779:{
4776:0
4770:x
4767:}
4757:{
4735:}
4726:x
4720:0
4717:{
4714:0
4708:x
4705:}
4696:0
4690:0
4687:{
4657:}
4648:x
4642:0
4639:{
4619:}
4610:x
4604:1
4598:{
4586:.
4574:}
4565:x
4559:0
4556:{
4553:1
4550:+
4547:x
4541:x
4538:}
4529:x
4523:1
4517:{
4495:}
4486:x
4480:0
4477:{
4474:1
4471:+
4468:x
4462:x
4459:}
4450:1
4447:+
4444:x
4438:0
4435:{
4406:x
4400:0
4390:P
4362:}
4353:x
4347:0
4344:{
4341:0
4335:x
4332:}
4326:=
4323:x
4320:{
4298:}
4289:x
4283:0
4280:{
4277:0
4271:x
4268:}
4259:x
4247:x
4241:0
4238:{
4208:}
4199:x
4193:0
4190:{
4187:1
4184:+
4181:x
4175:x
4172:}
4163:x
4157:0
4154:{
4132:}
4123:x
4117:0
4114:{
4111:1
4108:+
4105:x
4099:x
4096:}
4087:x
4075:x
4069:0
4066:{
4040:}
4031:x
4025:0
4022:{
4009:0
4003:x
3987:1
3984:+
3981:x
3975:x
3953:x
3940:}
3931:x
3925:0
3922:{
3886:2
3882:Q
3859:2
3855:P
3827:}
3822:1
3818:Q
3814:{
3811:S
3808:}
3803:1
3799:P
3795:{
3788:1
3784:Q
3775:2
3771:Q
3766:,
3762:}
3757:2
3753:Q
3749:{
3746:S
3743:}
3738:2
3734:P
3730:{
3726:,
3720:2
3716:P
3707:1
3703:P
3623:b
3620:;
3617:T
3601:b
3595:B
3579:;
3566:b
3563:;
3540:b
3537:;
3534:S
3518:b
3512:B
3499:;
3486:b
3440:T
3424:S
3408:B
3378:B
3374:P
3370:B
3346:Q
3325:}
3322:Q
3319:{
3306:T
3290:S
3274:B
3261:}
3258:P
3255:{
3250:}
3247:Q
3244:{
3241:T
3238:}
3235:P
3229:B
3223:{
3219:,
3215:}
3212:Q
3209:{
3206:S
3203:}
3200:P
3194:B
3191:{
3156:}
3150:=
3147:z
3144:{
3141:y
3135:z
3132:;
3129:1
3126:+
3123:x
3117:y
3114:}
3108:=
3105:1
3102:+
3099:x
3096:{
3070:}
3064:=
3061:z
3058:{
3055:y
3049:z
3046:}
3040:=
3037:y
3034:{
3008:}
3002:=
2999:y
2996:{
2993:1
2990:+
2987:x
2981:y
2978:}
2972:=
2969:1
2966:+
2963:x
2960:{
2930:}
2927:R
2924:{
2921:T
2918:;
2915:S
2912:}
2909:P
2906:{
2901:}
2898:R
2895:{
2892:T
2889:}
2886:Q
2883:{
2879:,
2875:}
2872:Q
2869:{
2866:S
2863:}
2860:P
2857:{
2836:Q
2834:(
2822:T
2819:;
2816:S
2806:T
2802:S
2798:T
2794:S
2771:}
2768:B
2765:=
2762:a
2756:A
2753:=
2750:b
2747:{
2717:b
2711:a
2705:a
2677:}
2674:B
2671:=
2668:b
2662:a
2656:A
2653:=
2650:b
2647:{
2617:;
2614:b
2608:a
2602:b
2574:}
2571:B
2568:=
2565:b
2559:A
2556:=
2553:b
2547:a
2544:{
2513:;
2510:b
2507:+
2504:a
2498:a
2470:}
2467:B
2464:=
2461:b
2455:A
2452:=
2449:a
2446:{
2397:a
2394:=
2391:b
2385:b
2382:+
2379:a
2359:b
2356:=
2353:)
2350:b
2344:a
2341:(
2335:a
2315:b
2309:a
2299:a
2295:B
2291:A
2287:b
2283:a
2279:b
2275:a
2241:}
2238:3
2235:=
2232:y
2229:{
2209:}
2206:]
2203:x
2199:/
2195:2
2192:[
2189:P
2186:{
2166:}
2163:P
2160:{
2146:y
2142:x
2125:}
2122:3
2119:=
2116:y
2113:{
2110:2
2104:x
2101:}
2098:3
2095:=
2092:y
2089:{
2054:}
2051:9
2045:y
2039:y
2033:y
2027:y
2021:0
2018:{
2015:y
2009:y
2003:x
2000:}
1997:9
1991:y
1985:y
1979:y
1973:y
1967:0
1964:{
1942:}
1939:9
1933:x
1927:y
1921:y
1915:0
1912:{
1909:y
1903:y
1897:x
1894:}
1891:9
1885:y
1879:y
1873:y
1867:y
1861:0
1858:{
1848:,
1836:}
1833:9
1827:y
1821:y
1815:x
1809:0
1806:{
1803:y
1797:y
1791:x
1788:}
1785:9
1779:y
1773:y
1767:y
1761:y
1755:0
1752:{
1742:,
1730:}
1727:9
1721:x
1715:x
1709:0
1706:{
1703:y
1697:y
1691:x
1688:}
1685:9
1679:y
1673:y
1667:y
1661:y
1655:0
1652:{
1627:]
1624:x
1620:/
1616:E
1613:[
1610:P
1600:P
1583:}
1580:1
1577:+
1574:x
1571:=
1568:x
1562:5
1559:=
1556:x
1553:{
1550:1
1547:+
1544:x
1538:x
1535:}
1532:5
1529:=
1526:x
1523:{
1500:}
1497:E
1494:=
1491:x
1485:P
1482:{
1479:E
1473:x
1470:}
1467:P
1464:{
1437:}
1434:5
1431:=
1428:3
1425:{
1422:3
1416:x
1413:}
1410:5
1407:=
1404:x
1401:{
1378:}
1375:]
1372:x
1368:/
1364:E
1361:[
1358:P
1355:{
1352:E
1346:x
1343:}
1340:P
1337:{
1306:=
1303:1
1300:+
1297:x
1274:=
1271:1
1268:+
1265:x
1242:=
1239:1
1236:+
1233:x
1213:]
1210:y
1206:/
1202:)
1199:1
1196:+
1193:x
1190:(
1187:[
1184:P
1161:=
1158:1
1155:+
1152:x
1129:=
1126:y
1116:P
1099:=
1096:1
1093:+
1090:x
1070:1
1067:+
1064:x
1058:y
1033:}
1030:N
1024:x
1021:{
1018:1
1015:+
1012:x
1006:x
1003:}
1000:N
994:1
991:+
988:x
985:{
964:}
958:=
955:y
952:{
949:1
946:+
943:x
937:y
934:}
928:=
925:1
922:+
919:x
916:{
898:P
884:]
881:x
877:/
873:E
870:[
867:P
844:]
841:x
837:/
833:E
830:[
827:P
817:P
803:]
800:x
796:/
792:E
789:[
786:P
776:P
762:]
759:x
755:/
751:E
748:[
745:P
732:E
724:x
716:P
702:]
699:x
695:/
691:E
688:[
685:P
658:}
655:P
652:{
649:E
643:x
640:}
637:]
634:x
630:/
626:E
623:[
620:P
617:{
595:x
591:P
565:}
562:P
559:{
549:}
546:P
543:{
489:R
469:R
466:}
463:Q
460:{
457:P
429:C
409:Q
389:Q
369:C
349:Q
329:C
309:P
228:Q
202:P
178:C
152:Q
132:P
109:}
106:Q
103:{
100:C
97:}
94:P
91:{
20:)
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.