Jennisys
This is where programs begin. Jennisys is a programming language that emphasizes clean public interfaces and lets programmers describe the data structures they intend a private implementation to use. Code is underemphasized, and Jennisys attempts to synthesize code automatically from the public interface and the given data-structure description.
Source and Tool
Jennisys is available as open source in the Boogie source repository, in the Jennisys directory. It is written in F# and it makes use of Dafny, which in turn rests on Boogie and Z3.
People
- K. Rustan M. Leino
- Aleksandar Milicevic (MIT)
People
Publications
- K. Rustan M. Leino and Aleksandar Milicevic, Program Extrapolation with Jennisys, no. MSR-TR-2012-12, February 2012
