Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1715631869132-->
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 **w**eakest **p**recondition.
Reference: Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1715631869137-->
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.
<!--ID: 1715631869141-->
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.
<!--ID: 1715631869144-->
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.
<!--ID: 1715631869148-->
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.
<!--ID: 1715631869153-->
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.
<!--ID: 1715631869157-->
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.
<!--ID: 1715631869161-->
END%%
%%ANKI
Basic
Given command $S$ and predicate $R$, what kind of mathematical object is $wp(S, R)$?
**Sequential composition** is one way of composing larger program segments from smaller segments. Let $S1$ and $S2$ be two commands. Then $S1; S2$ is defined as $$wp(''S1; S2'', R) = wp(S1, wp(S2, R))$$
%%ANKI
Basic
Let $S1$ and $S2$ be two commands. How is their sequential composition denoted?
Back: $S1; S2$
Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1719019485648-->
END%%
%%ANKI
Basic
How is $S1; S2$ defined in terms of $wp$?
Back: For any predicate $R$, $wp(''S1; S2'', R) = wp(S1, wp(S2, R))$.
Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1719019485654-->
END%%
%%ANKI
Basic
Is sequential composition commutative?
Back: No.
Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1719019485662-->
END%%
%%ANKI
Basic
Is sequential composition associative?
Back: Yes.
Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
The assignment command has form $x \coloneqq e$, provided the types of $x$ and $e$ are the same. This command is read as "$x$ becomes $e$" and is defined as $$wp(''x \coloneqq e'', R) = domain(e) \textbf{ cand } R_e^x$$
The multiple assignment command has form $$x_1 \circ s_1, \cdots, x_n \circ s_n \coloneqq e_1, \cdots, e_n$$
where each $x_i$ is an identifier, each $s_i$ is a [[equiv-trans#Selectors|selector]], and each expression $e_i$ has the same type as $x_i \circ s_i$. We denote this assignment more compactly as $\bar{x} \coloneqq \bar{e}$. We define multiple assignment as $$wp(''\bar{x} \coloneqq \bar{e}'', R) = domain(\bar{e}) \textbf{ cand } R_{\bar{e}}^\bar{x}$$
How is simple assignment $x \coloneqq e$ expressed in the following, more general form? $$x_1 \circ s_1, \ldots, x_n \circ s_n \coloneqq e_1, \ldots, e_n$$
How is simple assignment $b[i] \coloneqq e$ expressed in the following, more general form? $$x_1 \circ s_1, \ldots, x_n \circ s_n \coloneqq e_1, \ldots, e_n$$
The general form of the **alternative command** is: $$\begin{align*} \textbf{if } & B_1 \rightarrow S_1 \\ \textbf{ | } & B_2 \rightarrow S_2 \\ & \quad\cdots \\ \textbf{ | } & B_n \rightarrow S_n \\ \textbf{fi } & \end{align*}$$
Each $B_i \rightarrow S_i$ is called a **guarded command**. To execute the alternative command, find one true guard and execute the corresponding command. Notice this is nondeterministic. We denote the alternative command as $\text{IF}$ and define $\text{IF}$ in terms of $wp$ as: $$\begin{align*} wp(\text{IF}, R) = \;& (\forall i, 1 \leq i \leq n \Rightarrow domain(B_i)) \;\land \\ & (\exists i, 1 \leq i \leq n \land B_i) \;\land \\ & (\forall i, 1 \leq i \leq n \Rightarrow (B_i \Rightarrow wp(S_i, R))) \end{align*}$$
%%ANKI
Basic
How is the alternative command compactly denoted?
Back: As $\text{IF}$.
Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1722256345848-->
END%%
%%ANKI
Basic
What kind of command is $\text{IF}$ a representation of?
Back: An alternative command.
Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1722256906202-->
END%%
%%ANKI
Basic
What is the general form of the alternative command?
Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1722256345855-->
END%%
%%ANKI
Basic
What do "guarded commands" refer to?
Back: Each $B_i \rightarrow S_i$ found in the alternative command.
Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1722256345859-->
END%%
%%ANKI
Basic
*Why* are guarded commands named the way they are?
Back: The execution of the command is "guarded" by the truthiness of the condition.
Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1722256345863-->
END%%
%%ANKI
Basic
How are alternative commands executed?
Back: By finding any true guard and executing the corresponding command.
Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1722256345868-->
END%%
%%ANKI
Cloze
Consider $\text{IF}$ containing $B_i \rightarrow S_i$ for $1 \leq i \leq n$. Then $wp(\text{IF}, R)$ is the conjunction of:
* {$\forall i, 1 \leq i \leq n \Rightarrow domain(B_i)$}
* {$\exists i, 1 \leq i \leq n \land B_i$}
* {$\forall i, 1 \leq i \leq n \Rightarrow (B_i \Rightarrow wp(S_i, R))$}
Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1722256345873-->
END%%
%%ANKI
Basic
What assumption is made when defining $\text{IF}$ as follows? $$\begin{align*} wp(\text{IF}, R) = \;& (\exists i, 1 \leq i \leq n \land B_i) \;\land \\ & (\forall i, 1 \leq i \leq n \Rightarrow (B_i \Rightarrow wp(S_i, R))) \end{align*}$$
Back: $domain(B_i)$ for $1 \leq i \leq n$.
Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1722256906206-->
END%%
%%ANKI
Basic
Under what two conditions does the alternative command abort?
Back: If a condition isn't well-defined or no condition is satisfied.
Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1722256906210-->
END%%
%%ANKI
Basic
In what way is the alternative command's execution different from traditional case statements?
Back: It is nondeterministic.
Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1722256906214-->
END%%
%%ANKI
Basic
When *might* the following alternative command abort? $$\begin{align*} \textbf{if } & x > 0 \rightarrow z \coloneqq x \\ \textbf{ | } & x <0 \rightarrowz \coloneqq-x \\ \textbf{fi}& \end{align*}$$
Back: When $x = 0$.
Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1722257348944-->
END%%
%%ANKI
Basic
When is the first guarded command of the following executed? $$\begin{align*} \textbf{if } & x \geq 0 \rightarrow z \coloneqq x \\ \textbf{ | } & x \leq 0 \rightarrow z \coloneqq -x \\ \textbf{fi } & \end{align*}$$
Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1722257348955-->
END%%
%%ANKI
Basic
When are both of the following guarded commands executed? $$\begin{align*} \textbf{if } & x \geq 0 \rightarrow z \coloneqq x \\ \textbf{ | } & x \leq 0 \rightarrow z \coloneqq -x \\ \textbf{fi } & \end{align*}$$
Back: N/A.
Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1722257348960-->
END%%
%%ANKI
Basic
When are either of the following guarded commands executed? $$\begin{align*} \textbf{if } & x \geq 0 \rightarrow z \coloneqq x \\ \textbf{ | } & x \leq 0 \rightarrow z \coloneqq -x \\ \textbf{fi } & \end{align*}$$
Back: When $x = 0$.
Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1722257348966-->
END%%
%%ANKI
Cloze
Alternative command {$\textbf{if fi}$} is equivalent to command {$abort$}.
Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1722259243605-->
END%%
%%ANKI
Basic
*Why* does command $\textbf{if fi}$ abort?
Back: Because no guarded command is true (vacuously) by time of execution.
Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1722259243633-->
END%%
%%ANKI
Basic
How is command $skip$ wrapped in a no-op alternative command?
Back: As $\textbf{if } T \rightarrow skip \textbf{ fi}$
Reference: Gries, David.*The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
