Re: {Pre,Post}conditions and side effects

[Paul Rubin <no.email@nospam.invalid>]

"Randy Brukardt" <randy@rrsoftware.com> writes:
> Lastly, fancy proof languages tend to be beyond the skill level of ordinary 
> (and some not so ordinary) programmers. Despite, 6 years of University 
> education, a masters degree, and 30 years of real-world experience, I had to 
> have both the meaning of the implication operator and a "universally 
> quantified predicate" explained to me. As it turns out, I had run into both 
> in the past, but not under those names. 

I'd say there's two rather different approaches to verified software:
the approach based on Hoare logic (the precondition/postcondition stuff
as used in SPARK); and the approach based on dependent types, as used in
Coq.  Dependent types are the idea that you can have a typed lambda
calculus where the types are arbitrary predicates including quantified
ones involving other terms.  So if you have a term of a given type, that
constitutes a constructive proof of a value of that type.  By
typechecking the term and then compiling it into code, you have a
verified program that meets the specification expressed in the type.

The two approaches came out of different traditions so they tend to use
differing vocabulary (the stuff about quantified predicates is from
mathematical logic) but it's not that big a deal.  It sounds like you're
more familiar with the SPARK approach than the Coq approach, but I think
it's good to have some knowledge of both.

Note that dependent types can be arbitrary complicated, e.g. a Coq type
can express the execution semantics of a chunk of program code.  If you
can take a chunk of C code, assign semantics to it and label them with a
type, and transmogrify the C code until it's a chunk of assembly code
whose semantics have the same type as the C code as validated by a
typechecker, then you have a verified compiler.  This is basically how
CompCert (compcert.inria.fr) works.  The typechecker verifies that the
compiler output has preserved the meaning of the input source code.

You might like the online book "Software Foundations", which explains
writing verified code in Coq:

http://www.cis.upenn.edu/~bcpierce/sf/current/index.html

CompCert is one of Coq's success stories so Coq should be of
considerable interest to people interested in formal verification.

The book looks pretty accessible and working through it has been on my
infinite TODO list for quite a while.