I will first explain formal verification as applied to "normal" computer programs - that is, programs with only discrete state. The goal is, given a specification and a program, to prove that the program meets the specification. Consider the following simple example.
In industry, the standard is to check the desired property with unit tests, which offers some level of assurance, but does not preclude the existence of unchecked corner cases. This method of verification is also known as dynamic verification. For this project, I am focusing on computer-aided static verification, which tries to analyzes the program structure to try to prove assertions that hold for all possible executions. In order to do construct rigorous proofs of correctness, it is first necessary to be extremely precise in what the behavior of a program is. We then define a relatively complete set of rules for deducing that assertions will always be valid. This allows an automatic theorem prover which searches for derivations of assertions.
We will use a simple (but Turing complete language) called \(While\) defined by Winskel. The only datatype is an (arbitrary size) integer, variables cannot be dynamically allocated, and there are no functions. The only available loop is the while loop. The above Python program can be translated into \(While\) in a straight-forward manner.
We give semantics to programs in \(While\) by first defining the state \(\sigma\) of a program \(c\) as a function from variable names to integers (with undefined variables mapping to an arbitrary integer, say 0). We then write \([[c]]\) to denote a function from state to state which represents the semantics of \(c\). Some programs do not terminate, so there is a special state \(\bot\) (pronounced bottom) which represents the non-terminating state. As an illustration of these definitions, \([[x = 4]](\sigma)(x) = 4\) for \(\sigma \neq \bot\).
We can then define certain assertions as quantified boolean formulas (the "quantified" part means the formula can, for example, be \(\forall d \in \mathbb{N}. (\exists a, b \in \mathbb{N}. d \cdot a = m \land d \cdot b = n) \Rightarrow \exists c \in \mathbb{N}. d \cdot c = g\). This asserts that \(g = \gcd(m, n)\), or more literally, that if \(d\) is a divisor of \(m\) and \(n\), then \(d\) is also a divisor of \(g\).
We can also define rules for deducing that an assertion is valid. More generally (and more usefully) we define rules for deducing that an assertion is conditionally valid. That is, given a program fragment \(c\) and assertions \(A\) and \(B\), we say that \(\{A\}c\{B\}\) is a valid Hoare triple if whenever \(A\) holds, \(B\) will hold as well. This can be stated as \(A\) is a sufficient pre-condition for \(c\) to ensure the post-condition \(B\).
In logic, these rules of deduction are written as \(s_1, \ldots s_n \models s\), where the \(s_i\)'s are the (possibly empty) premises of the rule, and \(s\) is the conclusion. The rule means that whenever you have proven the premises are true, the conclusion is true as well.
Many deduction rules are straight-forward. For example, \((\{A\}c_1\{B\}, \{C\}c_2\{D\}, B \Rightarrow C) \models \{A\}c_1;c_2\{D\}\). This more or less states that if A implies B, B implies C, and C implies D, then A implies D.
The deduction rule for while loops, however, is a bit more involved. Suppose we are given a program of the form
Using these deduction rules, we can either try to:
a) prove that a certain precondition implies a certain postcondition for a piece of code or
b) given a desired postcondition, try to find the most general precondition that implies this postcondition.
Clearly b) is at least as hard as a), and it is the main goal of the tool I am developing.
In my next post, I'll write about some of the strategies we use.
# m and n are already defined
x = m
y = n
while x != 0:
if x >= y:
x, y = y, x
else:
y = y % x
# now y should be gcd(m, n)
In industry, the standard is to check the desired property with unit tests, which offers some level of assurance, but does not preclude the existence of unchecked corner cases. This method of verification is also known as dynamic verification. For this project, I am focusing on computer-aided static verification, which tries to analyzes the program structure to try to prove assertions that hold for all possible executions. In order to do construct rigorous proofs of correctness, it is first necessary to be extremely precise in what the behavior of a program is. We then define a relatively complete set of rules for deducing that assertions will always be valid. This allows an automatic theorem prover which searches for derivations of assertions.
We will use a simple (but Turing complete language) called \(While\) defined by Winskel. The only datatype is an (arbitrary size) integer, variables cannot be dynamically allocated, and there are no functions. The only available loop is the while loop. The above Python program can be translated into \(While\) in a straight-forward manner.
We give semantics to programs in \(While\) by first defining the state \(\sigma\) of a program \(c\) as a function from variable names to integers (with undefined variables mapping to an arbitrary integer, say 0). We then write \([[c]]\) to denote a function from state to state which represents the semantics of \(c\). Some programs do not terminate, so there is a special state \(\bot\) (pronounced bottom) which represents the non-terminating state. As an illustration of these definitions, \([[x = 4]](\sigma)(x) = 4\) for \(\sigma \neq \bot\).
We can then define certain assertions as quantified boolean formulas (the "quantified" part means the formula can, for example, be \(\forall d \in \mathbb{N}. (\exists a, b \in \mathbb{N}. d \cdot a = m \land d \cdot b = n) \Rightarrow \exists c \in \mathbb{N}. d \cdot c = g\). This asserts that \(g = \gcd(m, n)\), or more literally, that if \(d\) is a divisor of \(m\) and \(n\), then \(d\) is also a divisor of \(g\).
We can also define rules for deducing that an assertion is valid. More generally (and more usefully) we define rules for deducing that an assertion is conditionally valid. That is, given a program fragment \(c\) and assertions \(A\) and \(B\), we say that \(\{A\}c\{B\}\) is a valid Hoare triple if whenever \(A\) holds, \(B\) will hold as well. This can be stated as \(A\) is a sufficient pre-condition for \(c\) to ensure the post-condition \(B\).
In logic, these rules of deduction are written as \(s_1, \ldots s_n \models s\), where the \(s_i\)'s are the (possibly empty) premises of the rule, and \(s\) is the conclusion. The rule means that whenever you have proven the premises are true, the conclusion is true as well.
Many deduction rules are straight-forward. For example, \((\{A\}c_1\{B\}, \{C\}c_2\{D\}, B \Rightarrow C) \models \{A\}c_1;c_2\{D\}\). This more or less states that if A implies B, B implies C, and C implies D, then A implies D.
The deduction rule for while loops, however, is a bit more involved. Suppose we are given a program of the form
w = while(b) do cWe would like to deduce the validity of the Hoare triple \(\{A\}w\{B\}\). Essentially, we can deduce B if there using a loop invariant \(I\) and the termination condition \(\lnot b\). We will only give the rule for deducing partial correctness - that is, if the program terminates, then the result satisfies the postcondition. So \((A \Rightarrow I, \{I \land b\}c\{I\}, (I \land \lnot b) \Rightarrow B) \models \{A\}w\{B\}\). The most difficult part here is finding a suitable loop invariant. This is a fundamentally heuristic process, but there is a lot of literature on strategies for automatically finding invariant candidates.
Using these deduction rules, we can either try to:
a) prove that a certain precondition implies a certain postcondition for a piece of code or
b) given a desired postcondition, try to find the most general precondition that implies this postcondition.
Clearly b) is at least as hard as a), and it is the main goal of the tool I am developing.
In my next post, I'll write about some of the strategies we use.
