LXer: High integrity software
 

Published at LXer:

This book is the 2006 revision of the key guide to SPARK, a programming language founded on formal proof and static code analysis. This language happens to be implemented as an Ada dialect that makes use of formal comments to specify what the associated code is supposed to do, but it is not really Ada.

Read More...