Specifications and abstractions in Coq
======================================
Goal: reason about possible executions.
Same as in Butler's view.
Lower layer:
Code (implementation)
Concrete (code-level) states
Transition between code-level states,
dictated by execution semantics of code
Upper layer:
Code is the same, but we want to describe its behavior with a "spec"
Abstract states: just like Butler's lecture on Monday
connected to the code states using an abstraction relation (AR)
Transition between abstract-level states,
dictated by a specification of what this code should do
Goal: any code-level execution corresponds to a spec-level execution.
Intuitively matches the "trace-subset" property.
Although our Coq formalization doesn't have a notion of traces.
So what is a specification?
Abstraction for the state
Description of transitions for each piece of code ("procedure")
Abstraction of states
Nested: can continue to abstract at many levels
E.g., bare hardware states -> variable-level states -> StatDB-level state
Description of transitions
pre- and post-conditions
precondition may constrain the starting state
(or could be just True, if we have no constraints)
postcondition describes which final states are acceptable
could be non-deterministic: many final states are OK as far as the spec goes
postcondition also explicitly refers to the return value
same plan for describing transitions (pre and post conditions) works at any level
only difference: what type of state you're describing
code-level transitions: code-level state
abstract-level transitions: abstract state
What does it mean to prove that a piece of code satisfies a spec?
recall Butler's simulation "commutative diagram"
s ======> s'
^ ^^
| AR ||
V VV
c ------> c'
horizontal arrows are allowed transitions according to the spec (pre/post conditions)
vertical arrows are the abstraction relations between code and spec
single lines are given in the theorem:
suppose there is a code state "c", which transitions to state "c'"
and suppose there is a spec state "s" related to "c" by AR
double lines are what you have to prove:
show there exists a valid transition from "s" to "s'" according to spec pre/post conditions
and show that this same "s'" is related to "c'" using the AR
Can stack commutative diagrams in two ways
Side-by-side: combine two procedures with a semicolon
Sequential composition
What are the rules?
Postcondition of the first part must imply the precondition of the second part
One-above-another: provide an even higher-level specification, more abstraction
What are the rules?
AR types need to match up
Why preconditions?
More succinct spec
Does not specify what happens if precondition is violated
Might be fine, but assuming precondition might make for a simpler postcondition
Using procedure with a non-trivial precondition requires proving precondition holds
Typically useful for routines used in the middle of some code
E.g., in Butler's example of memory from last lecture:
in some cases, we know there's a free cache slot.
Easier to write a spec that says (precondition) "assuming there's a free cache slot",
(postcondition) "the cache will now contain XXX".
Example: variables, StatDB
StatDB state: list nat
Variable state: sum (nat), count (nat)
Abstraction relation: |l| = count /\ Sum(l) = sum
Code (only one piece of code):
add(x): sum += x; count += 1;
mean(): return sum/count;
Semantics for variables: let's assume they are obvious (will look at Coq code soon)
Semantics for StatDB:
mean():
PRE: True
POST: r = Sum(l) / |l|
/\ state' = state
add(x):
PRE: True
POST: state' = state ++ [x]
Diagram for mean
list l ===========================> list l'
^ ^^
| ||
V return sum/count VV
sum, count ---------------------> sum', count'
Proof:
Exists state? Yes, l' = l.
Exists relation? Yes, same relation.
Observe sum' = sum, count' = count, ..
Postcondition satisfied? Yes.
Diagram for add(x)
list l ====================================> list ??
^ ^^
| ||
V sum += x count += 1 VV
sum, count -----------> [?] ------------> sum', count'
Proof:
Exists state? Yes, l' = l ++ [x]
Exists relation? Yes, because:
Observe sum' = sum + x
Observe count' = count + 1
Relation matches l'
Postcondition satisfied? Yes.
What's going on with the middle state, [?]
sum? = sum + 1
count? = count
No matching abstract state
In our lab approach to modeling specs, it doesn't make sense
to peek inside the procedure's execution and describe it
using the abstract state. Valid AR re-established only
at procedure return.
Abstraction relation incorporates an invariant
i.e., some code states might not have a corresponding abstract states
concrete example from above, rather than just symbolic?
sum = 2
count = 0
also incorporate history variables, as Butler mentioned
many possible lists could correspond to the same sum/count code state
Initialization
Special kind of procedure
Starts with a code-level state
Returns a spec-level state (or a special return value indicating it didn't work)
One subtle issue in our model: representing that the code is always the same.
Abstraction levels can shift, specs can be different, but code is always code
For the same piece of code, can write different specs, at different abstraction levels
But need to agree that the same code always runs the same way, independent of abstraction
We define a basic type for state, called [world]
Axiom in Coq, not actually something that can be examined
Meant to represent the real state of the machine (and rest of world) where code runs
We define a basic type for how code looks like (procedures)
Also, mostly opaque in Coq
Meant to represent low-level Haskell code,
but we won't be reasoning about it directly
Except for two special operations:
Return a value
Connect two procedures together with a semicolon
This maps onto what Haskell calls the "IO monad"
Finally, we define an opaque semantics for how code runs
Again, defined via Axiom
Represents how Haskell runs the opaque low-level code
But we won't be reasoning about it directly
Our typical examples start by assuming there's already an abstraction stack,
from [world] to some simple state type, like variables in StatDB example/lab
Then we construct one more layer on top of that abstraction (e.g., StatDB).
Let's look at code:
VariablesAPI.
easy to miss detail: inited_any
StatDBAPI.
inited
Spec.Proc.
Crash handling largely irrelevant for now; will come back to it.
Spec.Abstraction.