10939
submission
Coryoth writes:
Traditionally if you want to write an avionics system for NASA you use formal methods and theorem provers at great expense, and if you want to write a business application you use an agile methodology and unit tests for a rapid feedback cycle. More recently, however, these seemingly incompatible approaches are coming together (PDF). The ESpec research project has put together an experimental system for Eiffel that, by extending unit tests with contracts, allows theorem proving to be integrated into an agile TDD system. ESpec provides a framework and tool suite that brings FIT acceptance testing, unit testing, design by contract, and theorem proving into a single environment with integrated reporting and fast turnaround. Given that more mature theorem provers already exist in ESC/Java2 for Java and Spec# for C#, surely it's only a matter of time before similar integrated systems appear for more popular languages.
10923
submission
Coryoth writes:
Agile development methods may soon incorporate automated theorem provers for code verification. The quality and efficiency of automated theorem provers for verifying code, such as ESC/Java2 and Spec#, have reached the point where they can be effectively integrated alongside unit tests in Agile methodology. Recent research papers have speculated that such integration could be highly beneficial and is almost inevitable. Could it be that theorem proving could become an integral part of Agile software development?
10809
submission
Coryoth writes:
Agile development and formal methods have generally been considered to be poles apart as far as software development methodologies go. It turns out that this is far from the case. Specification Driven Development(PDF) is an elegant marriage of Agile Test Driven Development with contract programming and lightweight formal methods. With high quality, fast, automated theorem provers making their way into the development world such as ESC/Java2 for Java, Spec# for C#, and ESpec for Eiffel, lightweight formal methods can be integrated into the Agile process. Espec provides an integrated system of Fit acceptance testing, unit testing, and theorem proving. Are similar integrated Agile specification based frameworks using JML and Spec# on the horizon for Java and C#?
9191
submission
Coryoth writes:
How do you convince co-workers of the benefits of extended static and runtime checking via contracts, and more detailed interface specification? Despite understanding the benefits static typing can provide for suitable projects, explaining the benefits of going one step further in specifying interfaces is proving difficult. Despite pragmatic systems like JML and Spec# which allow as much or as little extra specification as you need and still provide tangible benefits; despite automated theorem prover based systems, like ESC/Java2 and the Spec# verifier, which can do extensive checking statically and even produce potential counterexamples; fans of static type systems just don't seem to be able to see that their arguments for static rather than dynamic types apply equally well to contracts over static types alone. So what's the key to getting such people to consider stronger static checking?
7691
submission
Coryoth writes:
Literate Programs provides a growing wiki repository of well documented code. Articles are in literate programming style: a detailed plain english description of an algorithm with code samples interspersed. A click of the Download Code button will extract the code from the verbose documentation and provide you with straight code for you to play with. It's a repository of well documented algorithms complete with sample code; it's a repository to show off the style and functionality of a myriad of different programming languages (; It's a library of MIT licensed code for all your needs.
