Program Construction and Verification

algorithm alphabetic order and-E argument arithmetic array segment assignment axiom Assume begin end binary binary heap bubblesort cards chapter color(i compute conditional correctness conditional statements consequence rule consider cyclic codes defined degree(q(x denote Dijkstra disk elements equivalent even(k example executed Exercises false formal gold casket guarantee termination heapsort Horner's rule idempotent implication Induction step inductive reasoning inscription integer invariant property k-ary heap knave length logical mathematical induction middle deck MIN(i node number of occurrences odd(x P₁ path polynomial postcondition predicate prefix premise prevent evil problem proof rules propositional calculus prove q Q(i q*d+r range splitting remainder right decks rules of inference S₁ S₂ satisfying sequence sequential composition simplifies solution specification statement sum(i Superman Suppose termination condition true square truth table valid variables Variant verification conditions weakest precondition wp(if wp(S wp(S₁ wp(W