notebook/notes/programming/pred-trans.md

21 KiB

title TARGET DECK FILE TAGS tags
Predicate Transformers Obsidian::STEM programming::pred-trans
pred_trans
programming

Overview

Define \{Q\}\; S\; \{R\} as the predicate:

If execution of S is begun in a state satisfying Q, then it is guaranteed to terminate in a finite amount of time in a state satisfying R.

%%ANKI Basic What is Q in predicate \{Q\}\; S\; \{R\}? Back: A predicate. Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic What name is given to Q in \{Q\}\; S\; \{R\}? Back: The precondition of S. Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic What is R in predicate \{Q\}\; S\; \{R\}? Back: A predicate. Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic What name is given to R in \{Q\}\; S\; \{R\}? Back: The postcondition of S. Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic What is S in predicate \{Q\}\; S\; \{R\}? Back: A program (a sequence of statements). Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic What is the antecedent of \{Q\}\; S\; \{R\} in English? Back: S is executed in a state satisfying Q. Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic What is the consequent of \{Q\}\; S\; \{R\} in English? Back: S terminates in a finite amount of time in a state satisfying R. Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic How is \{Q\}\; S\; \{R\} defined? Back: If S is executed in a state satisfying Q, it eventually terminates in a state satisfying R. Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic How is \{x = X \land y = Y\}\; swap\; \{x = Y \land y = X\} rewritten without free identifiers? Back: \forall x, y, X, Y, \{x = X \land y = Y\}\; swap\; \{x = Y \land y = X\} Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic What name is given to X in e.g. \{x = X\}\; S\; \{y = Y\}? Back: The initial value of x. Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic How is \{Q\}\; S\; \{R\} augmented so that x has initial value X? Back: \{Q \land x = X\}\; S\; \{R\} Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic What name is given to Y in e.g. \{x = X\}\; S\; \{y = Y\}? Back: The final value of y. Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic How is \{Q\}\; S\; \{R\} augmented so that y has final value X? Back: \{Q\}\; S\; \{R \land y = X\} Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic How is \{Q\}\; S\; \{R\} augmented so that y has initial value X? Back: \{Q \land y = X\}\; S\; \{R\} Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic Why is \{T\}\; \text{while }T\text{ do skip}\; \{T\} everywhere false? Back: Because "\text{while }T\text{ do skip}" never terminates. Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

Weakest Precondition

For any command S and predicate R, we define the weakest precondition of S with respect to R, denoted wp(S, R), as

the set of all states such that execution of S begun in any one of them is guaranteed to terminate in a finite amount of time in a state satisfying R.

Expression \{Q\}\; S\; \{R\} is equivalent to Q \Rightarrow wp(S, R).

%%ANKI Basic What is the predicate transformer wp an acronym for? Back: The weakest precondition. Reference: Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic Given command S and predicate R, how is wp(S, R) defined? Back: As the set of all states such that execution of S in any one of them eventually terminates in a state satisfying R. Reference: Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic In terms of implications, how does a precondition compare to the weakest precondition? Back: A precondition implies the weakest precondition but not the other way around. Reference: Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic In terms of sets of states, how does a precondition compare to the weakest precondition? Back: A precondition represents a subset of the states the weakest precondition represents. Reference: Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic How is \{Q\}\; S\; \{R\} equivalently written as a predicate involving wp? Back: Q \Rightarrow wp(S, R) Reference: Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic How is Q \Rightarrow wp(S, R) equivalently written as a predicate using assertions? Back: \{Q\}\; S\; \{R\} Reference: Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic What kind of mathematical object is the wp transformer? Back: A function. Reference: Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic Given command S and predicate R, what kind of mathematical object is wp(S, R)? Back: A predicate, i.e. a set of states. Reference: Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic What does the term "predicate transformer" refer to? Back: A function that transforms one predicate into another. Reference: Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic What does the following evaluate to? $wp(''\text{if } x \geq y \text{ then } z := x \text{ else } z := y'', z = y)$ Back: y \geq x Reference: Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic What does the following evaluate to? $wp(''\text{if } x \geq y \text{ then } z := x \text{ else } z := y'', z = y - 1)$ Back: F Reference: Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic What does the following evaluate to? $wp(''\text{if } x \geq y \text{ then } z := x \text{ else } z := y'', z = y + 1)$ Back: x = y + 1 Reference: Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic What does the following evaluate to? $wp(''\text{if } x \geq y \text{ then } z := x \text{ else } z := y'', z = max(x, y))$ Back: T Reference: Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic Given command S, how is wp(S, T) interpreted? Back: As the set of all states such that execution of S in any of them terminates in a finite amount of time. Reference: Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

Law of the Excluded Miracle

Given any command S, $wp(S, F) = F$

%%ANKI Basic Given command S, what does wp(S, F) evaluate to? Back: F. Reference: Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic What does the Law of the Excluded Miracle state? Back: For any command S, wp(S, F) = F. Reference: Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic What name is given to identity wp(S, F) = F? Back: The Law of the Excluded Miracle. Reference: Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic Explain why the Law of the Excluded Miracle holds true. Back: No state satisfies F so no precondition can either. Reference: Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic Why is the Law of the Excluded Miracle named the way it is? Back: It would indeed be a miracle if execution could terminate in no state. Reference: Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic In Gries's exposition, is the Law of the Excluded Miracle taken as an axiom or a theorem? Back: An axiom. Reference: Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

Distributivity of Conjunction

Given command S and predicates Q and R, $wp(S, Q \land R) = wp(S, Q) \land wp(S, R)$

%%ANKI Basic What does Distributivity of Conjunction state? Back: Given command S and predicates Q and R, wp(S, Q \land R) = wp(S, Q) \land wp(S, R). Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Cloze Distributivity of Conjunction states {wp(S, Q \land R)} = {wp(S, Q) \land wp(S, R)}. Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic In Gries's exposition, is Distributivity of Conjunction taken as an axiom or a theorem? Back: An axiom. Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic Is wp(S, Q) \land wp(S, R) \Rightarrow wp(S, Q \land R) true if S is nondeterministic? Back: Yes. Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic Is wp(S, Q \land R) \Rightarrow wp(S, Q) \land wp(S, R) true if S is nondeterministic? Back: Yes. Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

Law of Monotonicity

Given command S and predicates Q and R, if Q \Rightarrow R, then wp(S, Q) \Rightarrow wp(S, R).

%%ANKI What does the Law of Monotonicity state? Back: Given command S and predicates Q and R, if Q \Rightarrow R, then wp(S, Q) \Rightarrow wp(S, R). Reference: Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981. END%%

%%ANKI Cloze Given command S, the Law of Monotonicity states that if {1:Q} \Rightarrow {2:R}, then {2:wp(S, Q)} \Rightarrow {1:wp(S, R)}. Reference: Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic In Gries's exposition, is the Law of Monotonicity taken as an axiom or a theorem? Back: A theorem. Reference: Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic Is the Law of Monotonicity true if the relevant command is nondeterministic? Back: Yes. Reference: Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

Distributivity of Disjunction

Given command S and predicates Q and R, $wp(S, Q) \lor wp(S, R) \Rightarrow wp(S, Q \lor R)$

%%ANKI Basic What does Distributivity of Disjunction state? Back: Given command S and predicates Q and R, wp(S, Q) \lor wp(S, R) \Rightarrow wp(S, Q \lor R). Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Cloze Distributivity of Disjunction states {1:wp(S, Q) \lor wp(S, r)} \Rightarrow {1:wp(S, Q \lor R)}. Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic In Gries's exposition, is Distributivity of Disjunction taken as an axiom or a theorem? Back: A theorem. Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic Assuming S is nondeterministic, is the following a tautology? $wp(S, Q \lor R) \Rightarrow wp(S, Q) \lor wp(S, R)$ Back: No. Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic Assuming S is nondeterministic, is the following a tautology? $wp(S, Q) \lor wp(S, R) \Rightarrow wp(S, Q \lor R)$ Back: Yes. Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic Assuming S is deterministic, is the following a tautology? $wp(S, Q \lor R) \Rightarrow wp(S, Q) \lor wp(S, R)$ Back: Yes. Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic Assuming S is deterministic, is the following a tautology? $wp(S, Q) \lor wp(S, R) \Rightarrow wp(S, Q \lor R)$ Back: Yes. Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic What command does Gries use to demonstrate nondeterminism? Back: The flipping of a coin. Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic What does it mean for command S to be nondeterministic? Back: Execution may not be the same even if begun in the same state. Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic Let S flip a coin and Q be flipping heads. What is wp(S, Q)? Back: F Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic Let S flip a coin and Q be flipping tails. What is wp(S, Q)? Back: F Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic Let S flip a coin, Q be flipping heads, and R be flipping tails. What is wp(S, Q \lor R)? Back: T Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic What constant operand evaluations determine the direction of implication in Distributivity of Disjunction? Back: F \Rightarrow T evaluates truthily but T \Rightarrow F does not. Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic Why does Distributivity of Disjunction use an implication instead of equality? Back: Because the underlying command may be nondeterministic. Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic When does Distributivity of Disjunction hold under equality (instead of implication)? Back: When the underlying command is deterministic. Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

Commands

skip

For any predicate R, wp(skip, R) = R.

%%ANKI Basic How is the skip command defined? Back: As wp(skip, R) = R. Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic Which command does Gries call the "identity transformation"? Back: skip Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Cloze Provide the specific command: for any predicate R, wp({skip}, R) = R. Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

abort

For any predicate R, wp(abort, R) = F.

%%ANKI Basic How is the abort command defined? Back: As wp(abort, R) = F. Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Cloze Provide the specific command: for any predicate R, wp({abort}, R) = F. Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic How is the abort command executed? Back: It isn't. Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic Why can't the abort command be executed? Back: By definition it executes in state F which is impossible. Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic Which command does Gries introduce as the only "constant" predicate transformer? Back: abort Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic How do we prove that abort is the only "constant" predicate transformer? Back: For any command S, the Law of the Excluded Miracle proves wp(S, F) = F. Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

%%ANKI Basic Suppose makeTrue is defined as wp(makeTrue, R) = T for all predicates R. What's wrong? Back: If R = F, makeTrue violates the Law of the Excluded Miracle. Reference: Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

END%%

Bibliography

  • Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.