{"id":170900,"date":"2012-02-07T12:00:26","date_gmt":"2012-02-07T12:00:26","guid":{"rendered":"https:\/\/www.microsoft.com\/en-us\/research\/project\/jennisys\/"},"modified":"2019-08-19T15:04:22","modified_gmt":"2019-08-19T22:04:22","slug":"jennisys","status":"publish","type":"msr-project","link":"https:\/\/www.microsoft.com\/en-us\/research\/project\/jennisys\/","title":{"rendered":"Jennisys"},"content":{"rendered":"<p>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.<\/p>\n<h2>Source and Tool<\/h2>\n<p>Jennisys is available as open source in the Boogie <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" target=\"_blank\" href=\"http:\/\/boogie.codeplex.com\/\">source repository<span class=\"sr-only\"> (opens in new tab)<\/span><\/a>, in the Jennisys directory.\u00a0 It is written in F# and it makes use of <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/project\/dafny-a-language-and-program-verifier-for-functional-correctness\/\">Dafny<\/a>, which in turn rests on <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/project\/boogie-an-intermediate-verification-language\/\">Boogie<\/a> and Z3.<\/p>\n<h2>Papers<\/h2>\n<ul>\n<li><em>Program Extrapolation with Jennisys<\/em>.\u00a0 K. Rustan M. Leino and Aleksandar Milicevic.\u00a0 (This is a newer version of the Technical Report below.)\u00a0 To appear, OOPSLA 2012.<\/li>\n<\/ul>\n","protected":false},"excerpt":{"rendered":"<p>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 [&hellip;]<\/p>\n","protected":false},"featured_media":0,"template":"","meta":{"msr-url-field":"","msr-podcast-episode":"","msrModifiedDate":"","msrModifiedDateEnabled":false,"ep_exclude_from_search":false,"_classifai_error":"","footnotes":""},"research-area":[13560],"msr-locale":[268875],"msr-impact-theme":[],"msr-pillar":[],"class_list":["post-170900","msr-project","type-msr-project","status-publish","hentry","msr-research-area-programming-languages-software-engineering","msr-locale-en_us","msr-archive-status-active"],"msr_project_start":"2012-02-07","related-publications":[162300],"related-downloads":[],"related-videos":[],"related-groups":[],"related-events":[],"related-opportunities":[],"related-posts":[],"related-articles":[],"tab-content":[],"slides":[],"related-researchers":[],"msr_research_lab":[],"msr_impact_theme":[],"_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/170900","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project"}],"about":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/types\/msr-project"}],"version-history":[{"count":2,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/170900\/revisions"}],"predecessor-version":[{"id":604350,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/170900\/revisions\/604350"}],"wp:attachment":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media?parent=170900"}],"wp:term":[{"taxonomy":"msr-research-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/research-area?post=170900"},{"taxonomy":"msr-locale","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-locale?post=170900"},{"taxonomy":"msr-impact-theme","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-impact-theme?post=170900"},{"taxonomy":"msr-pillar","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-pillar?post=170900"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}