...
The main tool we use is EventML which is a programming and specification language. EventML, built by Vinvent Rahli, cooperates with the Nuprl interactive theorem prover at every stage of program development to help programmers ensure correctness, document the code, and support modifications and improvements. It generates an Inductive Logical Form that proves the specification and can also automatically synthesize code.*
- Resources for EventML
...
- EventML documentation and downloads available at http://www.nuprl.org/software/
...
...
...
Code diversity is created during the process. We can introduce variants at: specification of classes, and code synthesis.
...