Saturday, December 14, 2013
how to do a design starting from a model that is gradually refined toward executable code
In this episode of Verification Corner, Jean-Raymond Abrial and Rustan Leino show how to do a design starting from a model that is gradually refined toward executable code. They use the Rodin tool, which supports the Event-B formalism.
Using an extended example that flattens and reconstructs trees, Sophia Drossopoulou and Rustan Leino show how to write inductive proofs of functional programs. The verification tool checks the correctness of the proofs. Proofs can be given in full detail, as they might be when a person first writes the proof or when the proof is intended for human understanding. Alternatively, proofs can be written with less detail, akin to the way a confident mathematician elides some details. In either case, the verification tool is satisfied only if it can fill in the missing pieces of the proof.
Jason Koenig and Rustan Leino show a verification problem that makes use of functions, ghost variables, and lemmas.
In this episode, Rosemary Monahan and Rustan Leino use problems specified using comprehension expressions to demonstrate how a problem can be solved using partial solutions