A Method of Programming

addop Algol 60 algorithm alternative statement annotated array of int ascending assertion assignment statement black nodes BO V B1 Boolean expression Boolean function calculation cistern concatenation conjunction declaration defined definition denote digit directly reachable disjunction domain elements end point euclid euclidplus example execution EXERCISE existential quantification f:swap(h false formal from(j functional specification grey nodes guarded command holds increment initial inner block integer expression intfactor introduced intterm invariant invercount lexicographic ordering Linear Search mathematical induction max(x maximal length means natural number number of iterations occur operators permissible expression postcondition postulate precondition predicate program that determines program to compute proof quantification Remark repetitive statement satisfies segment sequence of numbers sequence X(i shortest path skip statement list syntactic unit syntax termination to(j true universal quantification upsequence validity variables variant function Write a program ונ