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.
Papers
- Program Extrapolation with Jennisys. K. Rustan M. Leino and Aleksandar Milicevic. (This is a newer version of the Technical Report below.) To appear, OOPSLA 2012.