CINXE.COM

<!DOCTYPE html> <html class="client-nojs vector-feature-language-in-header-enabled vector-feature-language-in-main-page-header-disabled vector-feature-page-tools-pinned-disabled vector-feature-toc-pinned-clientpref-1 vector-feature-main-menu-pinned-disabled vector-feature-limited-width-clientpref-1 vector-feature-limited-width-content-enabled vector-feature-custom-font-size-clientpref-1 vector-feature-appearance-pinned-clientpref-1 vector-feature-night-mode-enabled skin-theme-clientpref-day vector-sticky-header-enabled vector-toc-available" lang="en" dir="ltr"> <head> <meta charset="UTF-8"> <title>Dafny - Wikipedia</title> <script>(function(){var className="client-js vector-feature-language-in-header-enabled vector-feature-language-in-main-page-header-disabled vector-feature-page-tools-pinned-disabled vector-feature-toc-pinned-clientpref-1 vector-feature-main-menu-pinned-disabled vector-feature-limited-width-clientpref-1 vector-feature-limited-width-content-enabled vector-feature-custom-font-size-clientpref-1 vector-feature-appearance-pinned-clientpref-1 vector-feature-night-mode-enabled skin-theme-clientpref-day vector-sticky-header-enabled vector-toc-available";var cookie=document.cookie.match(/(?:^|; )enwikimwclientpreferences=([^;]+)/);if(cookie){cookie[1].split('%2C').forEach(function(pref){className=className.replace(new RegExp('(^| )'+pref.replace(/-clientpref-\w+$|[^\w-]+/g,'')+'-clientpref-\\w+( |$)'),'$1'+pref+'$2');});}document.documentElement.className=className;}());RLCONF={"wgBreakFrames":false,"wgSeparatorTransformTable":["",""],"wgDigitTransformTable":["",""],"wgDefaultDateFormat":"dmy","wgMonthNames":["","January","February","March","April","May","June","July","August","September","October","November","December"],"wgRequestId":"cb43c326-915d-4d98-9ee0-53382d269d89","wgCanonicalNamespace":"","wgCanonicalSpecialPageName":false,"wgNamespaceNumber":0,"wgPageName":"Dafny","wgTitle":"Dafny","wgCurRevisionId":1265861302,"wgRevisionId":1265861302,"wgArticleId":56073623,"wgIsArticle":true,"wgIsRedirect":false,"wgAction":"view","wgUserName":null,"wgUserGroups":["*"],"wgCategories":["Articles with short description","Short description matches Wikidata","All articles with unsourced statements","Articles with unsourced statements from January 2023","Articles needing additional references from January 2018","All articles needing additional references","Academic programming languages","Experimental programming languages","Microsoft free software","Microsoft programming languages","Microsoft Research","Programming languages created in 2009","Proof assistants","Software using the MIT license","Statically typed programming languages"],"wgPageViewLanguage":"en","wgPageContentLanguage":"en","wgPageContentModel":"wikitext","wgRelevantPageName":"Dafny","wgRelevantArticleId":56073623,"wgIsProbablyEditable":true,"wgRelevantPageIsProbablyEditable":true,"wgRestrictionEdit":[],"wgRestrictionMove":[],"wgNoticeProject":"wikipedia","wgCiteReferencePreviewsActive":false,"wgFlaggedRevsParams":{"tags":{"status":{"levels":1}}},"wgMediaViewerOnClick":true,"wgMediaViewerEnabledByDefault":true,"wgPopupsFlags":0,"wgVisualEditor":{"pageLanguageCode":"en","pageLanguageDir":"ltr","pageVariantFallbacks":"en"},"wgMFDisplayWikibaseDescriptions":{"search":true,"watchlist":true,"tagline":false,"nearby":true},"wgWMESchemaEditAttemptStepOversample":false,"wgWMEPageLength":10000,"wgEditSubmitButtonLabelPublish":true,"wgULSPosition":"interlanguage","wgULSisCompactLinksEnabled":false,"wgVector2022LanguageInHeader":true,"wgULSisLanguageSelectorEmpty":false,"wgWikibaseItemId":"Q48989398","wgCheckUserClientHintsHeadersJsApi":["brands","architecture","bitness","fullVersionList","mobile","model","platform","platformVersion"],"GEHomepageSuggestedEditsEnableTopics":true,"wgGETopicsMatchModeEnabled":false,"wgGELevelingUpEnabledForUser":false}; RLSTATE={"ext.globalCssJs.user.styles":"ready","site.styles":"ready","user.styles":"ready","ext.globalCssJs.user":"ready","user":"ready","user.options":"loading","ext.cite.styles":"ready","ext.pygments":"ready","skins.vector.search.codex.styles":"ready","skins.vector.styles":"ready","skins.vector.icons":"ready","jquery.makeCollapsible.styles":"ready","ext.wikimediamessages.styles":"ready","ext.visualEditor.desktopArticleTarget.noscript":"ready","ext.uls.interlanguage":"ready","wikibase.client.init":"ready"};RLPAGEMODULES=["ext.cite.ux-enhancements","ext.pygments.view","site","mediawiki.page.ready","jquery.makeCollapsible","mediawiki.toc","skins.vector.js","ext.centralNotice.geoIP","ext.centralNotice.startUp","ext.gadget.ReferenceTooltips","ext.gadget.switcher","ext.urlShortener.toolbar","ext.centralauth.centralautologin","mmv.bootstrap","ext.popups","ext.visualEditor.desktopArticleTarget.init","ext.visualEditor.targetLoader","ext.echo.centralauth","ext.eventLogging","ext.wikimediaEvents","ext.navigationTiming","ext.uls.interface","ext.cx.eventlogging.campaigns","ext.cx.uls.quick.actions","wikibase.client.vector-2022","ext.checkUser.clientHints","ext.quicksurveys.init","ext.growthExperiments.SuggestedEditSession"];</script> <script>(RLQ=window.RLQ||[]).push(function(){mw.loader.impl(function(){return["user.options@12s5i",function($,jQuery,require,module){mw.user.tokens.set({"patrolToken":"+\\","watchToken":"+\\","csrfToken":"+\\"}); }];});});</script> <link rel="stylesheet" href="/w/load.php?lang=en&modules=ext.cite.styles%7Cext.pygments%7Cext.uls.interlanguage%7Cext.visualEditor.desktopArticleTarget.noscript%7Cext.wikimediamessages.styles%7Cjquery.makeCollapsible.styles%7Cskins.vector.icons%2Cstyles%7Cskins.vector.search.codex.styles%7Cwikibase.client.init&only=styles&skin=vector-2022"> <script async="" src="/w/load.php?lang=en&modules=startup&only=scripts&raw=1&skin=vector-2022"></script> <meta name="ResourceLoaderDynamicStyles" content=""> <link rel="stylesheet" href="/w/load.php?lang=en&modules=site.styles&only=styles&skin=vector-2022"> <meta name="generator" content="MediaWiki 1.44.0-wmf.22"> <meta name="referrer" content="origin"> <meta name="referrer" content="origin-when-cross-origin"> <meta name="robots" content="max-image-preview:standard"> <meta name="format-detection" content="telephone=no"> <meta property="og:image" content="https://upload.wikimedia.org/wikipedia/commons/4/44/Dafny_logo.jpg"> <meta property="og:image:width" content="1200"> <meta property="og:image:height" content="997"> <meta property="og:image" content="https://upload.wikimedia.org/wikipedia/commons/4/44/Dafny_logo.jpg"> <meta property="og:image:width" content="800"> <meta property="og:image:height" content="664"> <meta property="og:image" content="https://upload.wikimedia.org/wikipedia/commons/thumb/4/44/Dafny_logo.jpg/640px-Dafny_logo.jpg"> <meta property="og:image:width" content="640"> <meta property="og:image:height" content="531"> <meta name="viewport" content="width=1120"> <meta property="og:title" content="Dafny - Wikipedia"> <meta property="og:type" content="website"> <link rel="preconnect" href="//upload.wikimedia.org"> <link rel="alternate" media="only screen and (max-width: 640px)" href="//en.m.wikipedia.org/wiki/Dafny"> <link rel="alternate" type="application/x-wiki" title="Edit this page" href="/w/index.php?title=Dafny&action=edit"> <link rel="apple-touch-icon" href="/static/apple-touch/wikipedia.png"> <link rel="icon" href="/static/favicon/wikipedia.ico"> <link rel="search" type="application/opensearchdescription+xml" href="/w/rest.php/v1/search" title="Wikipedia (en)"> <link rel="EditURI" type="application/rsd+xml" href="//en.wikipedia.org/w/api.php?action=rsd"> <link rel="canonical" href="https://en.wikipedia.org/wiki/Dafny"> <link rel="license" href="https://creativecommons.org/licenses/by-sa/4.0/deed.en"> <link rel="alternate" type="application/atom+xml" title="Wikipedia Atom feed" href="/w/index.php?title=Special:RecentChanges&feed=atom"> <link rel="dns-prefetch" href="//meta.wikimedia.org" /> <link rel="dns-prefetch" href="auth.wikimedia.org"> </head> <body class="skin--responsive skin-vector skin-vector-search-vue mediawiki ltr sitedir-ltr mw-hide-empty-elt ns-0 ns-subject mw-editable page-Dafny rootpage-Dafny skin-vector-2022 action-view"><a class="mw-jump-link" href="#bodyContent">Jump to content</a> <div class="vector-header-container"> <header class="vector-header mw-header"> <div class="vector-header-start"> <nav class="vector-main-menu-landmark" aria-label="Site"> <div id="vector-main-menu-dropdown" class="vector-dropdown vector-main-menu-dropdown vector-button-flush-left vector-button-flush-right" title="Main menu" > <input type="checkbox" id="vector-main-menu-dropdown-checkbox" role="button" aria-haspopup="true" data-event-name="ui.dropdown-vector-main-menu-dropdown" class="vector-dropdown-checkbox " aria-label="Main menu" > <label id="vector-main-menu-dropdown-label" for="vector-main-menu-dropdown-checkbox" class="vector-dropdown-label cdx-button cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--weight-quiet cdx-button--icon-only " aria-hidden="true" ><span class="vector-icon mw-ui-icon-menu mw-ui-icon-wikimedia-menu"></span> <span class="vector-dropdown-label-text">Main menu</span> </label> <div class="vector-dropdown-content"> <div id="vector-main-menu-unpinned-container" class="vector-unpinned-container"> <div id="vector-main-menu" class="vector-main-menu vector-pinnable-element"> <div class="vector-pinnable-header vector-main-menu-pinnable-header vector-pinnable-header-unpinned" data-feature-name="main-menu-pinned" data-pinnable-element-id="vector-main-menu" data-pinned-container-id="vector-main-menu-pinned-container" data-unpinned-container-id="vector-main-menu-unpinned-container" > <div class="vector-pinnable-header-label">Main menu</div> <button class="vector-pinnable-header-toggle-button vector-pinnable-header-pin-button" data-event-name="pinnable-header.vector-main-menu.pin">move to sidebar</button> <button class="vector-pinnable-header-toggle-button vector-pinnable-header-unpin-button" data-event-name="pinnable-header.vector-main-menu.unpin">hide</button> </div> <div id="p-navigation" class="vector-menu mw-portlet mw-portlet-navigation" > <div class="vector-menu-heading"> Navigation </div> <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="n-mainpage-description" class="mw-list-item"><a href="/wiki/Main_Page" title="Visit the main page [z]" accesskey="z"><span>Main page</span></a></li><li id="n-contents" class="mw-list-item"><a href="/wiki/Wikipedia:Contents" title="Guides to browsing Wikipedia"><span>Contents</span></a></li><li id="n-currentevents" class="mw-list-item"><a href="/wiki/Portal:Current_events" title="Articles related to current events"><span>Current events</span></a></li><li id="n-randompage" class="mw-list-item"><a href="/wiki/Special:Random" title="Visit a randomly selected article [x]" accesskey="x"><span>Random article</span></a></li><li id="n-aboutsite" class="mw-list-item"><a href="/wiki/Wikipedia:About" title="Learn about Wikipedia and how it works"><span>About Wikipedia</span></a></li><li id="n-contactpage" class="mw-list-item"><a href="//en.wikipedia.org/wiki/Wikipedia:Contact_us" title="How to contact Wikipedia"><span>Contact us</span></a></li> </ul> </div> </div> <div id="p-interaction" class="vector-menu mw-portlet mw-portlet-interaction" > <div class="vector-menu-heading"> Contribute </div> <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="n-help" class="mw-list-item"><a href="/wiki/Help:Contents" title="Guidance on how to use and edit Wikipedia"><span>Help</span></a></li><li id="n-introduction" class="mw-list-item"><a href="/wiki/Help:Introduction" title="Learn how to edit Wikipedia"><span>Learn to edit</span></a></li><li id="n-portal" class="mw-list-item"><a href="/wiki/Wikipedia:Community_portal" title="The hub for editors"><span>Community portal</span></a></li><li id="n-recentchanges" class="mw-list-item"><a href="/wiki/Special:RecentChanges" title="A list of recent changes to Wikipedia [r]" accesskey="r"><span>Recent changes</span></a></li><li id="n-upload" class="mw-list-item"><a href="/wiki/Wikipedia:File_upload_wizard" title="Add images or other media for use on Wikipedia"><span>Upload file</span></a></li><li id="n-specialpages" class="mw-list-item"><a href="/wiki/Special:SpecialPages"><span>Special pages</span></a></li> </ul> </div> </div> </div> </div> </div> </div> </nav> <a href="/wiki/Main_Page" class="mw-logo"> <img class="mw-logo-icon" src="/static/images/icons/wikipedia.png" alt="" aria-hidden="true" height="50" width="50"> <span class="mw-logo-container skin-invert"> <img class="mw-logo-wordmark" alt="Wikipedia" src="/static/images/mobile/copyright/wikipedia-wordmark-en.svg" style="width: 7.5em; height: 1.125em;"> <img class="mw-logo-tagline" alt="The Free Encyclopedia" src="/static/images/mobile/copyright/wikipedia-tagline-en.svg" width="117" height="13" style="width: 7.3125em; height: 0.8125em;"> </span> </a> </div> <div class="vector-header-end"> <div id="p-search" role="search" class="vector-search-box-vue vector-search-box-collapses vector-search-box-show-thumbnail vector-search-box-auto-expand-width vector-search-box"> <a href="/wiki/Special:Search" class="cdx-button cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--weight-quiet cdx-button--icon-only search-toggle" title="Search Wikipedia [f]" accesskey="f"><span class="vector-icon mw-ui-icon-search mw-ui-icon-wikimedia-search"></span> <span>Search</span> </a> <div class="vector-typeahead-search-container"> <div class="cdx-typeahead-search cdx-typeahead-search--show-thumbnail cdx-typeahead-search--auto-expand-width"> <form action="/w/index.php" id="searchform" class="cdx-search-input cdx-search-input--has-end-button"> <div id="simpleSearch" class="cdx-search-input__input-wrapper" data-search-loc="header-moved"> <div class="cdx-text-input cdx-text-input--has-start-icon"> <input class="cdx-text-input__input" type="search" name="search" placeholder="Search Wikipedia" aria-label="Search Wikipedia" autocapitalize="sentences" title="Search Wikipedia [f]" accesskey="f" id="searchInput" > <span class="cdx-text-input__icon cdx-text-input__start-icon"></span> </div> <input type="hidden" name="title" value="Special:Search"> </div> <button class="cdx-button cdx-search-input__end-button">Search</button> </form> </div> </div> </div> <nav class="vector-user-links vector-user-links-wide" aria-label="Personal tools"> <div class="vector-user-links-main"> <div id="p-vector-user-menu-preferences" class="vector-menu mw-portlet emptyPortlet" > <div class="vector-menu-content"> <ul class="vector-menu-content-list"> </ul> </div> </div> <div id="p-vector-user-menu-userpage" class="vector-menu mw-portlet emptyPortlet" > <div class="vector-menu-content"> <ul class="vector-menu-content-list"> </ul> </div> </div> <nav class="vector-appearance-landmark" aria-label="Appearance"> <div id="vector-appearance-dropdown" class="vector-dropdown " title="Change the appearance of the page's font size, width, and color" > <input type="checkbox" id="vector-appearance-dropdown-checkbox" role="button" aria-haspopup="true" data-event-name="ui.dropdown-vector-appearance-dropdown" class="vector-dropdown-checkbox " aria-label="Appearance" > <label id="vector-appearance-dropdown-label" for="vector-appearance-dropdown-checkbox" class="vector-dropdown-label cdx-button cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--weight-quiet cdx-button--icon-only " aria-hidden="true" ><span class="vector-icon mw-ui-icon-appearance mw-ui-icon-wikimedia-appearance"></span> <span class="vector-dropdown-label-text">Appearance</span> </label> <div class="vector-dropdown-content"> <div id="vector-appearance-unpinned-container" class="vector-unpinned-container"> </div> </div> </div> </nav> <div id="p-vector-user-menu-notifications" class="vector-menu mw-portlet emptyPortlet" > <div class="vector-menu-content"> <ul class="vector-menu-content-list"> </ul> </div> </div> <div id="p-vector-user-menu-overflow" class="vector-menu mw-portlet" > <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="pt-sitesupport-2" class="user-links-collapsible-item mw-list-item user-links-collapsible-item"><a data-mw="interface" href="https://donate.wikimedia.org/?wmf_source=donate&wmf_medium=sidebar&wmf_campaign=en.wikipedia.org&uselang=en" class=""><span>Donate</span></a> </li> <li id="pt-createaccount-2" class="user-links-collapsible-item mw-list-item user-links-collapsible-item"><a data-mw="interface" href="/w/index.php?title=Special:CreateAccount&returnto=Dafny" title="You are encouraged to create an account and log in; however, it is not mandatory" class=""><span>Create account</span></a> </li> <li id="pt-login-2" class="user-links-collapsible-item mw-list-item user-links-collapsible-item"><a data-mw="interface" href="/w/index.php?title=Special:UserLogin&returnto=Dafny" title="You're encouraged to log in; however, it's not mandatory. [o]" accesskey="o" class=""><span>Log in</span></a> </li> </ul> </div> </div> </div> <div id="vector-user-links-dropdown" class="vector-dropdown vector-user-menu vector-button-flush-right vector-user-menu-logged-out" title="Log in and more options" > <input type="checkbox" id="vector-user-links-dropdown-checkbox" role="button" aria-haspopup="true" data-event-name="ui.dropdown-vector-user-links-dropdown" class="vector-dropdown-checkbox " aria-label="Personal tools" > <label id="vector-user-links-dropdown-label" for="vector-user-links-dropdown-checkbox" class="vector-dropdown-label cdx-button cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--weight-quiet cdx-button--icon-only " aria-hidden="true" ><span class="vector-icon mw-ui-icon-ellipsis mw-ui-icon-wikimedia-ellipsis"></span> <span class="vector-dropdown-label-text">Personal tools</span> </label> <div class="vector-dropdown-content"> <div id="p-personal" class="vector-menu mw-portlet mw-portlet-personal user-links-collapsible-item" title="User menu" > <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="pt-sitesupport" class="user-links-collapsible-item mw-list-item"><a href="https://donate.wikimedia.org/?wmf_source=donate&wmf_medium=sidebar&wmf_campaign=en.wikipedia.org&uselang=en"><span>Donate</span></a></li><li id="pt-createaccount" class="user-links-collapsible-item mw-list-item"><a href="/w/index.php?title=Special:CreateAccount&returnto=Dafny" title="You are encouraged to create an account and log in; however, it is not mandatory"><span class="vector-icon mw-ui-icon-userAdd mw-ui-icon-wikimedia-userAdd"></span> <span>Create account</span></a></li><li id="pt-login" class="user-links-collapsible-item mw-list-item"><a href="/w/index.php?title=Special:UserLogin&returnto=Dafny" title="You're encouraged to log in; however, it's not mandatory. [o]" accesskey="o"><span class="vector-icon mw-ui-icon-logIn mw-ui-icon-wikimedia-logIn"></span> <span>Log in</span></a></li> </ul> </div> </div> <div id="p-user-menu-anon-editor" class="vector-menu mw-portlet mw-portlet-user-menu-anon-editor" > <div class="vector-menu-heading"> Pages for logged out editors <a href="/wiki/Help:Introduction" aria-label="Learn more about editing"><span>learn more</span></a> </div> <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="pt-anoncontribs" class="mw-list-item"><a href="/wiki/Special:MyContributions" title="A list of edits made from this IP address [y]" accesskey="y"><span>Contributions</span></a></li><li id="pt-anontalk" class="mw-list-item"><a href="/wiki/Special:MyTalk" title="Discussion about edits from this IP address [n]" accesskey="n"><span>Talk</span></a></li> </ul> </div> </div> </div> </div> </nav> </div> </header> </div> <div class="mw-page-container"> <div class="mw-page-container-inner"> <div class="vector-sitenotice-container"> <div id="siteNotice"></div> </div> <div class="vector-column-start"> <div class="vector-main-menu-container"> <div id="mw-navigation"> <nav id="mw-panel" class="vector-main-menu-landmark" aria-label="Site"> <div id="vector-main-menu-pinned-container" class="vector-pinned-container"> </div> </nav> </div> </div> <div class="vector-sticky-pinned-container"> <nav id="mw-panel-toc" aria-label="Contents" data-event-name="ui.sidebar-toc" class="mw-table-of-contents-container vector-toc-landmark"> <div id="vector-toc-pinned-container" class="vector-pinned-container"> <div id="vector-toc" class="vector-toc vector-pinnable-element"> <div class="vector-pinnable-header vector-toc-pinnable-header vector-pinnable-header-pinned" data-feature-name="toc-pinned" data-pinnable-element-id="vector-toc" > <h2 class="vector-pinnable-header-label">Contents</h2> <button class="vector-pinnable-header-toggle-button vector-pinnable-header-pin-button" data-event-name="pinnable-header.vector-toc.pin">move to sidebar</button> <button class="vector-pinnable-header-toggle-button vector-pinnable-header-unpin-button" data-event-name="pinnable-header.vector-toc.unpin">hide</button> </div> <ul class="vector-toc-contents" id="mw-panel-toc-list"> <li id="toc-mw-content-text" class="vector-toc-list-item vector-toc-level-1"> <a href="#" class="vector-toc-link"> <div class="vector-toc-text">(Top)</div> </a> </li> <li id="toc-Data_types" class="vector-toc-list-item vector-toc-level-1 vector-toc-list-item-expanded"> <a class="vector-toc-link" href="#Data_types"> <div class="vector-toc-text"> <span class="vector-toc-numb">1</span> <span>Data types</span> </div> </a> <ul id="toc-Data_types-sublist" class="vector-toc-list"> </ul> </li> <li id="toc-Imperative_features" class="vector-toc-list-item vector-toc-level-1 vector-toc-list-item-expanded"> <a class="vector-toc-link" href="#Imperative_features"> <div class="vector-toc-text"> <span class="vector-toc-numb">2</span> <span>Imperative features</span> </div> </a> <ul id="toc-Imperative_features-sublist" class="vector-toc-list"> </ul> </li> <li id="toc-Loop_invariants" class="vector-toc-list-item vector-toc-level-1 vector-toc-list-item-expanded"> <a class="vector-toc-link" href="#Loop_invariants"> <div class="vector-toc-text"> <span class="vector-toc-numb">3</span> <span>Loop invariants</span> </div> </a> <ul id="toc-Loop_invariants-sublist" class="vector-toc-list"> </ul> </li> <li id="toc-Proof_features" class="vector-toc-list-item vector-toc-level-1 vector-toc-list-item-expanded"> <a class="vector-toc-link" href="#Proof_features"> <div class="vector-toc-text"> <span class="vector-toc-numb">4</span> <span>Proof features</span> </div> </a> <ul id="toc-Proof_features-sublist" class="vector-toc-list"> </ul> </li> <li id="toc-See_also" class="vector-toc-list-item vector-toc-level-1 vector-toc-list-item-expanded"> <a class="vector-toc-link" href="#See_also"> <div class="vector-toc-text"> <span class="vector-toc-numb">5</span> <span>See also</span> </div> </a> <ul id="toc-See_also-sublist" class="vector-toc-list"> </ul> </li> <li id="toc-References" class="vector-toc-list-item vector-toc-level-1 vector-toc-list-item-expanded"> <a class="vector-toc-link" href="#References"> <div class="vector-toc-text"> <span class="vector-toc-numb">6</span> <span>References</span> </div> </a> <ul id="toc-References-sublist" class="vector-toc-list"> </ul> </li> <li id="toc-Further_reading" class="vector-toc-list-item vector-toc-level-1 vector-toc-list-item-expanded"> <a class="vector-toc-link" href="#Further_reading"> <div class="vector-toc-text"> <span class="vector-toc-numb">7</span> <span>Further reading</span> </div> </a> <ul id="toc-Further_reading-sublist" class="vector-toc-list"> </ul> </li> <li id="toc-External_links" class="vector-toc-list-item vector-toc-level-1 vector-toc-list-item-expanded"> <a class="vector-toc-link" href="#External_links"> <div class="vector-toc-text"> <span class="vector-toc-numb">8</span> <span>External links</span> </div> </a> <ul id="toc-External_links-sublist" class="vector-toc-list"> </ul> </li> </ul> </div> </div> </nav> </div> </div> <div class="mw-content-container"> <main id="content" class="mw-body"> <header class="mw-body-header vector-page-titlebar"> <nav aria-label="Contents" class="vector-toc-landmark"> <div id="vector-page-titlebar-toc" class="vector-dropdown vector-page-titlebar-toc vector-button-flush-left" title="Table of Contents" > <input type="checkbox" id="vector-page-titlebar-toc-checkbox" role="button" aria-haspopup="true" data-event-name="ui.dropdown-vector-page-titlebar-toc" class="vector-dropdown-checkbox " aria-label="Toggle the table of contents" > <label id="vector-page-titlebar-toc-label" for="vector-page-titlebar-toc-checkbox" class="vector-dropdown-label cdx-button cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--weight-quiet cdx-button--icon-only " aria-hidden="true" ><span class="vector-icon mw-ui-icon-listBullet mw-ui-icon-wikimedia-listBullet"></span> <span class="vector-dropdown-label-text">Toggle the table of contents</span> </label> <div class="vector-dropdown-content"> <div id="vector-page-titlebar-toc-unpinned-container" class="vector-unpinned-container"> </div> </div> </div> </nav> <h1 id="firstHeading" class="firstHeading mw-first-heading"><span class="mw-page-title-main">Dafny</span></h1> <div id="p-lang-btn" class="vector-dropdown mw-portlet mw-portlet-lang" > <input type="checkbox" id="p-lang-btn-checkbox" role="button" aria-haspopup="true" data-event-name="ui.dropdown-p-lang-btn" class="vector-dropdown-checkbox mw-interlanguage-selector" aria-label="Go to an article in another language. Available in 3 languages" > <label id="p-lang-btn-label" for="p-lang-btn-checkbox" class="vector-dropdown-label cdx-button cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--weight-quiet cdx-button--action-progressive mw-portlet-lang-heading-3" aria-hidden="true" ><span class="vector-icon mw-ui-icon-language-progressive mw-ui-icon-wikimedia-language-progressive"></span> <span class="vector-dropdown-label-text">3 languages</span> </label> <div class="vector-dropdown-content"> <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li class="interlanguage-link interwiki-et mw-list-item"><a href="https://et.wikipedia.org/wiki/Dafny" title="Dafny – Estonian" lang="et" hreflang="et" data-title="Dafny" data-language-autonym="Eesti" data-language-local-name="Estonian" class="interlanguage-link-target"><span>Eesti</span></a></li><li class="interlanguage-link interwiki-es mw-list-item"><a href="https://es.wikipedia.org/wiki/Dafny" title="Dafny – Spanish" lang="es" hreflang="es" data-title="Dafny" data-language-autonym="Español" data-language-local-name="Spanish" class="interlanguage-link-target"><span>Español</span></a></li><li class="interlanguage-link interwiki-eu mw-list-item"><a href="https://eu.wikipedia.org/wiki/Dafny" title="Dafny – Basque" lang="eu" hreflang="eu" data-title="Dafny" data-language-autonym="Euskara" data-language-local-name="Basque" class="interlanguage-link-target"><span>Euskara</span></a></li> </ul> <div class="after-portlet after-portlet-lang"><span class="wb-langlinks-edit wb-langlinks-link"><a href="https://www.wikidata.org/wiki/Special:EntityPage/Q48989398#sitelinks-wikipedia" title="Edit interlanguage links" class="wbc-editpage">Edit links</a></span></div> </div> </div> </div> </header> <div class="vector-page-toolbar"> <div class="vector-page-toolbar-container"> <div id="left-navigation"> <nav aria-label="Namespaces"> <div id="p-associated-pages" class="vector-menu vector-menu-tabs mw-portlet mw-portlet-associated-pages" > <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="ca-nstab-main" class="selected vector-tab-noicon mw-list-item"><a href="/wiki/Dafny" title="View the content page [c]" accesskey="c"><span>Article</span></a></li><li id="ca-talk" class="vector-tab-noicon mw-list-item"><a href="/wiki/Talk:Dafny" rel="discussion" title="Discuss improvements to the content page [t]" accesskey="t"><span>Talk</span></a></li> </ul> </div> </div> <div id="vector-variants-dropdown" class="vector-dropdown emptyPortlet" > <input type="checkbox" id="vector-variants-dropdown-checkbox" role="button" aria-haspopup="true" data-event-name="ui.dropdown-vector-variants-dropdown" class="vector-dropdown-checkbox " aria-label="Change language variant" > <label id="vector-variants-dropdown-label" for="vector-variants-dropdown-checkbox" class="vector-dropdown-label cdx-button cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--weight-quiet" aria-hidden="true" ><span class="vector-dropdown-label-text">English</span> </label> <div class="vector-dropdown-content"> <div id="p-variants" class="vector-menu mw-portlet mw-portlet-variants emptyPortlet" > <div class="vector-menu-content"> <ul class="vector-menu-content-list"> </ul> </div> </div> </div> </div> </nav> </div> <div id="right-navigation" class="vector-collapsible"> <nav aria-label="Views"> <div id="p-views" class="vector-menu vector-menu-tabs mw-portlet mw-portlet-views" > <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="ca-view" class="selected vector-tab-noicon mw-list-item"><a href="/wiki/Dafny"><span>Read</span></a></li><li id="ca-edit" class="vector-tab-noicon mw-list-item"><a href="/w/index.php?title=Dafny&action=edit" title="Edit this page [e]" accesskey="e"><span>Edit</span></a></li><li id="ca-history" class="vector-tab-noicon mw-list-item"><a href="/w/index.php?title=Dafny&action=history" title="Past revisions of this page [h]" accesskey="h"><span>View history</span></a></li> </ul> </div> </div> </nav> <nav class="vector-page-tools-landmark" aria-label="Page tools"> <div id="vector-page-tools-dropdown" class="vector-dropdown vector-page-tools-dropdown" > <input type="checkbox" id="vector-page-tools-dropdown-checkbox" role="button" aria-haspopup="true" data-event-name="ui.dropdown-vector-page-tools-dropdown" class="vector-dropdown-checkbox " aria-label="Tools" > <label id="vector-page-tools-dropdown-label" for="vector-page-tools-dropdown-checkbox" class="vector-dropdown-label cdx-button cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--weight-quiet" aria-hidden="true" ><span class="vector-dropdown-label-text">Tools</span> </label> <div class="vector-dropdown-content"> <div id="vector-page-tools-unpinned-container" class="vector-unpinned-container"> <div id="vector-page-tools" class="vector-page-tools vector-pinnable-element"> <div class="vector-pinnable-header vector-page-tools-pinnable-header vector-pinnable-header-unpinned" data-feature-name="page-tools-pinned" data-pinnable-element-id="vector-page-tools" data-pinned-container-id="vector-page-tools-pinned-container" data-unpinned-container-id="vector-page-tools-unpinned-container" > <div class="vector-pinnable-header-label">Tools</div> <button class="vector-pinnable-header-toggle-button vector-pinnable-header-pin-button" data-event-name="pinnable-header.vector-page-tools.pin">move to sidebar</button> <button class="vector-pinnable-header-toggle-button vector-pinnable-header-unpin-button" data-event-name="pinnable-header.vector-page-tools.unpin">hide</button> </div> <div id="p-cactions" class="vector-menu mw-portlet mw-portlet-cactions emptyPortlet vector-has-collapsible-items" title="More options" > <div class="vector-menu-heading"> Actions </div> <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="ca-more-view" class="selected vector-more-collapsible-item mw-list-item"><a href="/wiki/Dafny"><span>Read</span></a></li><li id="ca-more-edit" class="vector-more-collapsible-item mw-list-item"><a href="/w/index.php?title=Dafny&action=edit" title="Edit this page [e]" accesskey="e"><span>Edit</span></a></li><li id="ca-more-history" class="vector-more-collapsible-item mw-list-item"><a href="/w/index.php?title=Dafny&action=history"><span>View history</span></a></li> </ul> </div> </div> <div id="p-tb" class="vector-menu mw-portlet mw-portlet-tb" > <div class="vector-menu-heading"> General </div> <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="t-whatlinkshere" class="mw-list-item"><a href="/wiki/Special:WhatLinksHere/Dafny" title="List of all English Wikipedia pages containing links to this page [j]" accesskey="j"><span>What links here</span></a></li><li id="t-recentchangeslinked" class="mw-list-item"><a href="/wiki/Special:RecentChangesLinked/Dafny" rel="nofollow" title="Recent changes in pages linked from this page [k]" accesskey="k"><span>Related changes</span></a></li><li id="t-upload" class="mw-list-item"><a href="//en.wikipedia.org/wiki/Wikipedia:File_Upload_Wizard" title="Upload files [u]" accesskey="u"><span>Upload file</span></a></li><li id="t-permalink" class="mw-list-item"><a href="/w/index.php?title=Dafny&oldid=1265861302" title="Permanent link to this revision of this page"><span>Permanent link</span></a></li><li id="t-info" class="mw-list-item"><a href="/w/index.php?title=Dafny&action=info" title="More information about this page"><span>Page information</span></a></li><li id="t-cite" class="mw-list-item"><a href="/w/index.php?title=Special:CiteThisPage&page=Dafny&id=1265861302&wpFormIdentifier=titleform" title="Information on how to cite this page"><span>Cite this page</span></a></li><li id="t-urlshortener" class="mw-list-item"><a href="/w/index.php?title=Special:UrlShortener&url=https%3A%2F%2Fen.wikipedia.org%2Fwiki%2FDafny"><span>Get shortened URL</span></a></li><li id="t-urlshortener-qrcode" class="mw-list-item"><a href="/w/index.php?title=Special:QrCode&url=https%3A%2F%2Fen.wikipedia.org%2Fwiki%2FDafny"><span>Download QR code</span></a></li> </ul> </div> </div> <div id="p-coll-print_export" class="vector-menu mw-portlet mw-portlet-coll-print_export" > <div class="vector-menu-heading"> Print/export </div> <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="coll-download-as-rl" class="mw-list-item"><a href="/w/index.php?title=Special:DownloadAsPdf&page=Dafny&action=show-download-screen" title="Download this page as a PDF file"><span>Download as PDF</span></a></li><li id="t-print" class="mw-list-item"><a href="/w/index.php?title=Dafny&printable=yes" title="Printable version of this page [p]" accesskey="p"><span>Printable version</span></a></li> </ul> </div> </div> <div id="p-wikibase-otherprojects" class="vector-menu mw-portlet mw-portlet-wikibase-otherprojects" > <div class="vector-menu-heading"> In other projects </div> <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="t-wikibase" class="wb-otherproject-link wb-otherproject-wikibase-dataitem mw-list-item"><a href="https://www.wikidata.org/wiki/Special:EntityPage/Q48989398" title="Structured data on this page hosted by Wikidata [g]" accesskey="g"><span>Wikidata item</span></a></li> </ul> </div> </div> </div> </div> </div> </div> </nav> </div> </div> </div> <div class="vector-column-end"> <div class="vector-sticky-pinned-container"> <nav class="vector-page-tools-landmark" aria-label="Page tools"> <div id="vector-page-tools-pinned-container" class="vector-pinned-container"> </div> </nav> <nav class="vector-appearance-landmark" aria-label="Appearance"> <div id="vector-appearance-pinned-container" class="vector-pinned-container"> <div id="vector-appearance" class="vector-appearance vector-pinnable-element"> <div class="vector-pinnable-header vector-appearance-pinnable-header vector-pinnable-header-pinned" data-feature-name="appearance-pinned" data-pinnable-element-id="vector-appearance" data-pinned-container-id="vector-appearance-pinned-container" data-unpinned-container-id="vector-appearance-unpinned-container" > <div class="vector-pinnable-header-label">Appearance</div> <button class="vector-pinnable-header-toggle-button vector-pinnable-header-pin-button" data-event-name="pinnable-header.vector-appearance.pin">move to sidebar</button> <button class="vector-pinnable-header-toggle-button vector-pinnable-header-unpin-button" data-event-name="pinnable-header.vector-appearance.unpin">hide</button> </div> </div> </div> </nav> </div> </div> <div id="bodyContent" class="vector-body" aria-labelledby="firstHeading" data-mw-ve-target-container> <div class="vector-body-before-content"> <div class="mw-indicators"> </div> <div id="siteSub" class="noprint">From Wikipedia, the free encyclopedia</div> </div> <div id="contentSub"><div id="mw-content-subtitle"></div></div> <div id="mw-content-text" class="mw-body-content"><div class="mw-content-ltr mw-parser-output" lang="en" dir="ltr"><div class="shortdescription nomobile noexcerpt noprint searchaux" style="display:none">Programming language</div> <style data-mw-deduplicate="TemplateStyles:r1257001546">.mw-parser-output .infobox-subbox{padding:0;border:none;margin:-3px;width:auto;min-width:100%;font-size:100%;clear:none;float:none;background-color:transparent}.mw-parser-output .infobox-3cols-child{margin:auto}.mw-parser-output .infobox .navbar{font-size:100%}@media screen{html.skin-theme-clientpref-night .mw-parser-output .infobox-full-data:not(.notheme)>div:not(.notheme)[style]{background:#1f1f23!important;color:#f8f9fa}}@media screen and (prefers-color-scheme:dark){html.skin-theme-clientpref-os .mw-parser-output .infobox-full-data:not(.notheme) div:not(.notheme){background:#1f1f23!important;color:#f8f9fa}}@media(min-width:640px){body.skin--responsive .mw-parser-output .infobox-table{display:table!important}body.skin--responsive .mw-parser-output .infobox-table>caption{display:table-caption!important}body.skin--responsive .mw-parser-output .infobox-table>tbody{display:table-row-group}body.skin--responsive .mw-parser-output .infobox-table tr{display:table-row!important}body.skin--responsive .mw-parser-output .infobox-table th,body.skin--responsive .mw-parser-output .infobox-table td{padding-left:inherit;padding-right:inherit}}</style><table class="infobox vevent"><caption class="infobox-title summary">Dafny</caption><tbody><tr><td colspan="2" class="infobox-image"><span typeof="mw:File"><a href="/wiki/File:Dafny_logo.jpg" class="mw-file-description"><img src="//upload.wikimedia.org/wikipedia/commons/thumb/4/44/Dafny_logo.jpg/250px-Dafny_logo.jpg" decoding="async" width="128" height="106" class="mw-file-element" srcset="//upload.wikimedia.org/wikipedia/commons/thumb/4/44/Dafny_logo.jpg/330px-Dafny_logo.jpg 2x" data-file-width="690" data-file-height="573" /></a></span></td></tr><tr><th scope="row" class="infobox-label"><a href="/wiki/Programming_paradigm" title="Programming paradigm">Paradigm</a></th><td class="infobox-data"><a href="/wiki/Imperative_programming" title="Imperative programming">Imperative</a>, <a href="/wiki/Functional_programming_language" class="mw-redirect" title="Functional programming language">functional</a></td></tr><tr><th scope="row" class="infobox-label"><a href="/wiki/Software_design" title="Software design">Designed by</a></th><td class="infobox-data">K. Rustan M. Leino</td></tr><tr><th scope="row" class="infobox-label"><a href="/wiki/Software_developer" class="mw-redirect" title="Software developer">Developer</a></th><td class="infobox-data organiser"><a href="/wiki/Microsoft_Research" title="Microsoft Research">Microsoft Research</a></td></tr><tr><th scope="row" class="infobox-label">First appeared</th><td class="infobox-data">2009<span class="noprint">; 16 years ago</span><span style="display:none"> (<span class="bday dtstart published updated">2009</span>)</span></td></tr><tr><td colspan="2" class="infobox-full-data"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1257001546" /></td></tr><tr><th scope="row" class="infobox-label" style="white-space: nowrap;"><a href="/wiki/Software_release_life_cycle" title="Software release life cycle">Stable release</a></th><td class="infobox-data"><div style="margin:0px;">4.9.0 / October 31, 2024<span class="noprint">; 5 months ago</span><span style="display:none"> (<span class="bday dtstart published updated">2024-10-31</span>)</span></div></td></tr><tr style="display:none"><td colspan="2"> </td></tr><tr><th scope="row" class="infobox-label"><a href="/wiki/Type_system" title="Type system">Typing discipline</a></th><td class="infobox-data"><a href="/wiki/Type_system" title="Type system">Static, strong, safe</a></td></tr><tr><th scope="row" class="infobox-label"><a href="/wiki/Software_license" title="Software license">License</a></th><td class="infobox-data"><a href="/wiki/MIT_License" title="MIT License">MIT License</a></td></tr><tr><th scope="row" class="infobox-label"><a href="/wiki/Filename_extension" title="Filename extension">Filename extensions</a></th><td class="infobox-data">.dfy</td></tr><tr><th scope="row" class="infobox-label">Website</th><td class="infobox-data"><span class="url"><a rel="nofollow" class="external text" href="https://dafny.org/">dafny<wbr />.org</a></span></td></tr></tbody></table> <p><b>Dafny</b> is an <a href="/wiki/Imperative_programming" title="Imperative programming">imperative</a> and <a href="/wiki/Functional_programming_language" class="mw-redirect" title="Functional programming language">functional</a> <a href="/wiki/Compiled_programming_language" class="mw-redirect" title="Compiled programming language">compiled language</a> that compiles to other <a href="/wiki/Programming_language" title="Programming language">programming languages</a>, such as <a href="/wiki/C_Sharp_(programming_language)" title="C Sharp (programming language)">C#</a>, <a href="/wiki/Java_(programming_language)" title="Java (programming language)">Java</a>, <a href="/wiki/JavaScript" title="JavaScript">JavaScript</a>, <a href="/wiki/Go_(programming_language)" title="Go (programming language)">Go</a> and <a href="/wiki/Python_(programming_language)" title="Python (programming language)">Python</a>. It supports <a href="/wiki/Formal_specification" title="Formal specification">formal specification</a> through <a href="/wiki/Preconditions" class="mw-redirect" title="Preconditions">preconditions</a>, <a href="/wiki/Postconditions" class="mw-redirect" title="Postconditions">postconditions</a>, <a href="/wiki/Loop_invariant" title="Loop invariant">loop invariants</a>, <a href="/wiki/Loop_variant" title="Loop variant">loop variants</a>, termination specifications and read/write framing specifications. The language combines ideas from the <a href="/wiki/Functional_programming" title="Functional programming">functional</a> and <a href="/wiki/Imperative_programming" title="Imperative programming">imperative</a> paradigms; it includes support for <a href="/wiki/Object-oriented_programming" title="Object-oriented programming">object-oriented programming</a>. Features include <i>generic classes</i>, <i>dynamic allocation</i>, <i>inductive datatypes</i> and a variation of <a href="/wiki/Separation_logic" title="Separation logic">separation logic</a> known as <i>implicit dynamic frames</i><sup id="cite_ref-1" class="reference"><a href="#cite_note-1"><span class="cite-bracket">[</span>1<span class="cite-bracket">]</span></a></sup> for reasoning about side effects.<sup id="cite_ref-2" class="reference"><a href="#cite_note-2"><span class="cite-bracket">[</span>2<span class="cite-bracket">]</span></a></sup> Dafny was created by Rustan Leino at <a href="/wiki/Microsoft_Research" title="Microsoft Research">Microsoft Research</a> after his previous work on developing ESC/Modula-3, <a href="/wiki/ESC/Java" title="ESC/Java">ESC/Java</a>, and Spec#. </p><p>Dafny is widely used in teaching<sup class="noprint Inline-Template Template-Fact" style="white-space:nowrap;">[<i><a href="/wiki/Wikipedia:Citation_needed" title="Wikipedia:Citation needed"><span title="This claim needs references to reliable sources. (January 2023)">citation needed</span></a></i>]</sup> because it provides a simple, integrated introduction to formal specification and verification; it is regularly featured in software verification competitions (e.g. VSTTE'08,<sup id="cite_ref-3" class="reference"><a href="#cite_note-3"><span class="cite-bracket">[</span>3<span class="cite-bracket">]</span></a></sup> VSCOMP'10,<sup id="cite_ref-4" class="reference"><a href="#cite_note-4"><span class="cite-bracket">[</span>4<span class="cite-bracket">]</span></a></sup> COST'11,<sup id="cite_ref-5" class="reference"><a href="#cite_note-5"><span class="cite-bracket">[</span>5<span class="cite-bracket">]</span></a></sup> and VerifyThis'12<sup id="cite_ref-6" class="reference"><a href="#cite_note-6"><span class="cite-bracket">[</span>6<span class="cite-bracket">]</span></a></sup>). </p><p>Dafny was designed as a verification-aware programming language, requiring verification along with code development. It thus fits the "Correct by Construction" software development paradigm. Verification proofs are supported by a mathematical toolbox that includes mathematical integers and reals, bit-vectors, sequences, sets, multisets, infinite sequences and sets, induction, co-induction, and calculational proofs. Verification obligations are discharged automatically, given sufficient specification. Dafny uses some program analysis to infer many specification assertions, reducing the burden on the user of writing specifications. The general proof framework is that of <a href="/wiki/Hoare_logic" title="Hoare logic">Hoare logic</a>. </p><p>Dafny builds on the Boogie <a href="/wiki/Intermediate_language" class="mw-redirect" title="Intermediate language">intermediate language</a> which uses the <a href="/wiki/Z3_Theorem_Prover" title="Z3 Theorem Prover">Z3 automated theorem prover</a> for discharging proof obligations.<sup id="cite_ref-7" class="reference"><a href="#cite_note-7"><span class="cite-bracket">[</span>7<span class="cite-bracket">]</span></a></sup><sup id="cite_ref-8" class="reference"><a href="#cite_note-8"><span class="cite-bracket">[</span>8<span class="cite-bracket">]</span></a></sup> </p> <meta property="mw:PageProp/toc" /> <div class="mw-heading mw-heading2"><h2 id="Data_types">Data types</h2><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Dafny&action=edit&section=1" title="Edit section: Data types"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <style data-mw-deduplicate="TemplateStyles:r1251242444">.mw-parser-output .ambox{border:1px solid #a2a9b1;border-left:10px solid #36c;background-color:#fbfbfb;box-sizing:border-box}.mw-parser-output .ambox+link+.ambox,.mw-parser-output .ambox+link+style+.ambox,.mw-parser-output .ambox+link+link+.ambox,.mw-parser-output .ambox+.mw-empty-elt+link+.ambox,.mw-parser-output .ambox+.mw-empty-elt+link+style+.ambox,.mw-parser-output .ambox+.mw-empty-elt+link+link+.ambox{margin-top:-1px}html body.mediawiki .mw-parser-output .ambox.mbox-small-left{margin:4px 1em 4px 0;overflow:hidden;width:238px;border-collapse:collapse;font-size:88%;line-height:1.25em}.mw-parser-output .ambox-speedy{border-left:10px solid #b32424;background-color:#fee7e6}.mw-parser-output .ambox-delete{border-left:10px solid #b32424}.mw-parser-output .ambox-content{border-left:10px solid #f28500}.mw-parser-output .ambox-style{border-left:10px solid #fc3}.mw-parser-output .ambox-move{border-left:10px solid #9932cc}.mw-parser-output .ambox-protection{border-left:10px solid #a2a9b1}.mw-parser-output .ambox .mbox-text{border:none;padding:0.25em 0.5em;width:100%}.mw-parser-output .ambox .mbox-image{border:none;padding:2px 0 2px 0.5em;text-align:center}.mw-parser-output .ambox .mbox-imageright{border:none;padding:2px 0.5em 2px 0;text-align:center}.mw-parser-output .ambox .mbox-empty-cell{border:none;padding:0;width:1px}.mw-parser-output .ambox .mbox-image-div{width:52px}@media(min-width:720px){.mw-parser-output .ambox{margin:0 10%}}@media print{body.ns-0 .mw-parser-output .ambox{display:none!important}}</style><table class="box-Unreferenced_section plainlinks metadata ambox ambox-content ambox-Unreferenced" role="presentation"><tbody><tr><td class="mbox-image"><div class="mbox-image-div"><span typeof="mw:File"><a href="/wiki/File:Question_book-new.svg" class="mw-file-description"><img alt="" src="//upload.wikimedia.org/wikipedia/en/thumb/9/99/Question_book-new.svg/50px-Question_book-new.svg.png" decoding="async" width="50" height="39" class="mw-file-element" srcset="//upload.wikimedia.org/wikipedia/en/thumb/9/99/Question_book-new.svg/75px-Question_book-new.svg.png 1.5x, //upload.wikimedia.org/wikipedia/en/thumb/9/99/Question_book-new.svg/100px-Question_book-new.svg.png 2x" data-file-width="512" data-file-height="399" /></a></span></div></td><td class="mbox-text"><div class="mbox-text-span">This section <b>does not <a href="/wiki/Wikipedia:Citing_sources" title="Wikipedia:Citing sources">cite</a> any <a href="/wiki/Wikipedia:Verifiability" title="Wikipedia:Verifiability">sources</a></b>.<span class="hide-when-compact"> Please help <a href="/wiki/Special:EditPage/Dafny" title="Special:EditPage/Dafny">improve this section</a> by <a href="/wiki/Help:Referencing_for_beginners" title="Help:Referencing for beginners">adding citations to reliable sources</a>. Unsourced material may be challenged and <a href="/wiki/Wikipedia:Verifiability#Burden_of_evidence" title="Wikipedia:Verifiability">removed</a>.</span> <span class="date-container"><i>(<span class="date">January 2018</span>)</i></span><span class="hide-when-compact"><i> (<small><a href="/wiki/Help:Maintenance_template_removal" title="Help:Maintenance template removal">Learn how and when to remove this message</a></small>)</i></span></div></td></tr></tbody></table> <p>Dafny provides methods for implementation which may have <a href="/wiki/Side_effect_(computer_science)" title="Side effect (computer science)">side-effects</a> and functions for use in specification which are <a href="/wiki/Pure_function" title="Pure function">pure</a>.<sup id="cite_ref-9" class="reference"><a href="#cite_note-9"><span class="cite-bracket">[</span>9<span class="cite-bracket">]</span></a></sup> Methods consist of sequences of statements following a familiar imperative style whilst, in contrast, the body of a function is simply an expression. Any side-effecting statements in a method (e.g. assigning an element of an array parameter) must be accounted for by noting which parameters can be mutated, using the <code>modifies</code> clause. Dafny also provides a range of <i>immutable</i> collection types including: sequences (e.g. <code>seq<int></code>), sets (e.g. <code>set<int></code>), maps (<code>map<int,int></code>), tuples, inductive datatypes and <i>mutable</i> arrays (e.g. <code>array<int></code>). </p> <div class="mw-heading mw-heading2"><h2 id="Imperative_features">Imperative features</h2><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Dafny&action=edit&section=2" title="Edit section: Imperative features"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1251242444" /><table class="box-Unreferenced_section plainlinks metadata ambox ambox-content ambox-Unreferenced" role="presentation"><tbody><tr><td class="mbox-image"><div class="mbox-image-div"><span typeof="mw:File"><a href="/wiki/File:Question_book-new.svg" class="mw-file-description"><img alt="" src="//upload.wikimedia.org/wikipedia/en/thumb/9/99/Question_book-new.svg/50px-Question_book-new.svg.png" decoding="async" width="50" height="39" class="mw-file-element" srcset="//upload.wikimedia.org/wikipedia/en/thumb/9/99/Question_book-new.svg/75px-Question_book-new.svg.png 1.5x, //upload.wikimedia.org/wikipedia/en/thumb/9/99/Question_book-new.svg/100px-Question_book-new.svg.png 2x" data-file-width="512" data-file-height="399" /></a></span></div></td><td class="mbox-text"><div class="mbox-text-span">This section <b>does not <a href="/wiki/Wikipedia:Citing_sources" title="Wikipedia:Citing sources">cite</a> any <a href="/wiki/Wikipedia:Verifiability" title="Wikipedia:Verifiability">sources</a></b>.<span class="hide-when-compact"> Please help <a href="/wiki/Special:EditPage/Dafny" title="Special:EditPage/Dafny">improve this section</a> by <a href="/wiki/Help:Referencing_for_beginners" title="Help:Referencing for beginners">adding citations to reliable sources</a>. Unsourced material may be challenged and <a href="/wiki/Wikipedia:Verifiability#Burden_of_evidence" title="Wikipedia:Verifiability">removed</a>.</span> <span class="date-container"><i>(<span class="date">January 2018</span>)</i></span><span class="hide-when-compact"><i> (<small><a href="/wiki/Help:Maintenance_template_removal" title="Help:Maintenance template removal">Learn how and when to remove this message</a></small>)</i></span></div></td></tr></tbody></table> <p>The following illustrates many of the features in Dafny, including the use of preconditions, postconditions, loop invariants and loop variants. </p> <div class="mw-highlight mw-highlight-lang-java mw-content-ltr" dir="ltr"><pre><span></span><span class="n">method</span><span class="w"> </span><span class="nf">max</span><span class="p">(</span><span class="n">arr</span><span class="p">:</span><span class="n">array</span><span class="o"><</span><span class="kt">int</span><span class="o">></span><span class="p">)</span><span class="w"> </span><span class="n">returns</span><span class="w"> </span><span class="p">(</span><span class="n">max</span><span class="p">:</span><span class="kt">int</span><span class="p">)</span> <span class="w"> </span><span class="c1">// Array must have at least one element</span> <span class="w"> </span><span class="n">requires</span><span class="w"> </span><span class="n">arr</span><span class="p">.</span><span class="na">Length</span><span class="w"> </span><span class="o">></span><span class="w"> </span><span class="mi">0</span> <span class="w"> </span><span class="c1">// Return cannot be smaller than any element in array</span> <span class="w"> </span><span class="n">ensures</span><span class="w"> </span><span class="n">forall</span><span class="w"> </span><span class="n">j</span><span class="w"> </span><span class="p">:</span><span class="w"> </span><span class="kt">int</span><span class="w"> </span><span class="p">::</span><span class="w"> </span><span class="n">j</span><span class="w"> </span><span class="o">>=</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="o">&&</span><span class="w"> </span><span class="n">j</span><span class="w"> </span><span class="o"><</span><span class="w"> </span><span class="n">arr</span><span class="p">.</span><span class="na">Length</span><span class="w"> </span><span class="o">==></span><span class="w"> </span><span class="n">max</span><span class="w"> </span><span class="o">>=</span><span class="w"> </span><span class="n">arr</span><span class="o">[</span><span class="n">j</span><span class="o">]</span> <span class="w"> </span><span class="c1">// Return must match some element in array</span> <span class="w"> </span><span class="n">ensures</span><span class="w"> </span><span class="n">exists</span><span class="w"> </span><span class="n">j</span><span class="w"> </span><span class="p">:</span><span class="w"> </span><span class="kt">int</span><span class="w"> </span><span class="p">::</span><span class="w"> </span><span class="n">j</span><span class="o">>=</span><span class="mi">0</span><span class="w"> </span><span class="o">&&</span><span class="w"> </span><span class="n">j</span><span class="w"> </span><span class="o"><</span><span class="w"> </span><span class="n">arr</span><span class="p">.</span><span class="na">Length</span><span class="w"> </span><span class="o">&&</span><span class="w"> </span><span class="n">max</span><span class="w"> </span><span class="o">==</span><span class="w"> </span><span class="n">arr</span><span class="o">[</span><span class="n">j</span><span class="o">]</span> <span class="p">{</span> <span class="w"> </span><span class="n">max</span><span class="w"> </span><span class="p">:</span><span class="o">=</span><span class="w"> </span><span class="n">arr</span><span class="o">[</span><span class="mi">0</span><span class="o">]</span><span class="p">;</span> <span class="w"> </span><span class="kd">var</span><span class="w"> </span><span class="n">i</span><span class="p">:</span><span class="w"> </span><span class="kt">int</span><span class="w"> </span><span class="p">:</span><span class="o">=</span><span class="w"> </span><span class="mi">1</span><span class="p">;</span> <span class="w"> </span><span class="c1">//</span> <span class="w"> </span><span class="k">while</span><span class="p">(</span><span class="n">i</span><span class="w"> </span><span class="o"><</span><span class="w"> </span><span class="n">arr</span><span class="p">.</span><span class="na">Length</span><span class="p">)</span> <span class="w"> </span><span class="c1">// Index at most arr.Length (needed to show i==arr.Length after loop)</span> <span class="w"> </span><span class="n">invariant</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="o"><=</span><span class="w"> </span><span class="n">arr</span><span class="p">.</span><span class="na">Length</span> <span class="w"> </span><span class="c1">// No element seen so far larger than max</span> <span class="w"> </span><span class="n">invariant</span><span class="w"> </span><span class="n">forall</span><span class="w"> </span><span class="n">j</span><span class="p">:</span><span class="kt">int</span><span class="w"> </span><span class="p">::</span><span class="w"> </span><span class="n">j</span><span class="w"> </span><span class="o">>=</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="o">&&</span><span class="w"> </span><span class="n">j</span><span class="w"> </span><span class="o"><</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="o">==></span><span class="w"> </span><span class="n">max</span><span class="w"> </span><span class="o">>=</span><span class="w"> </span><span class="n">arr</span><span class="o">[</span><span class="n">j</span><span class="o">]</span> <span class="w"> </span><span class="c1">// Some element seen so far matches max</span> <span class="w"> </span><span class="n">invariant</span><span class="w"> </span><span class="n">exists</span><span class="w"> </span><span class="n">j</span><span class="p">:</span><span class="kt">int</span><span class="w"> </span><span class="p">::</span><span class="w"> </span><span class="n">j</span><span class="w"> </span><span class="o">>=</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="o">&&</span><span class="w"> </span><span class="n">j</span><span class="w"> </span><span class="o"><</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="o">&&</span><span class="w"> </span><span class="n">max</span><span class="w"> </span><span class="o">==</span><span class="w"> </span><span class="n">arr</span><span class="o">[</span><span class="n">j</span><span class="o">]</span> <span class="w"> </span><span class="c1">// arr.Length - i decreases at every step and is lower-bounded by 0</span> <span class="w"> </span><span class="n">decreases</span><span class="w"> </span><span class="n">arr</span><span class="p">.</span><span class="na">Length</span><span class="w"> </span><span class="o">-</span><span class="w"> </span><span class="n">i</span> <span class="w"> </span><span class="p">{</span> <span class="w"> </span><span class="c1">// Update max if larger element encountered</span> <span class="w"> </span><span class="k">if</span><span class="w"> </span><span class="p">(</span><span class="n">arr</span><span class="o">[</span><span class="n">i</span><span class="o">]</span><span class="w"> </span><span class="o">></span><span class="w"> </span><span class="n">max</span><span class="p">)</span><span class="w"> </span><span class="p">{</span> <span class="w"> </span><span class="n">max</span><span class="w"> </span><span class="p">:</span><span class="o">=</span><span class="w"> </span><span class="n">arr</span><span class="o">[</span><span class="n">i</span><span class="o">]</span><span class="p">;</span> <span class="w"> </span><span class="p">}</span> <span class="w"> </span><span class="c1">// Continue through array</span> <span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="p">:</span><span class="o">=</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="o">+</span><span class="w"> </span><span class="mi">1</span><span class="p">;</span> <span class="w"> </span><span class="p">}</span> <span class="p">}</span> </pre></div> <p>This example computes the maximum element of an array. The method's precondition and postcondition are given with the <code>requires</code> and <code>ensures</code> clauses (respectively). Likewise, the loop invariant and loop variant are given through the <code>invariant</code> and <code>decreases</code> clauses (respectively). </p> <div class="mw-heading mw-heading2"><h2 id="Loop_invariants">Loop invariants</h2><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Dafny&action=edit&section=3" title="Edit section: Loop invariants"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <p>The treatment of loop invariants in Dafny differs from traditional <a href="/wiki/Hoare_logic" title="Hoare logic">Hoare logic</a>. Variables mutated in a loop are treated such that (most) information known about them prior to the loop is discarded. Information required to prove properties of such variables must be expressed explicitly in the loop invariant. In contrast, variables not mutated in the loop retain all information known about them beforehand. The following example illustrates using loops: </p> <div class="mw-highlight mw-highlight-lang-java mw-content-ltr" dir="ltr"><pre><span></span><span class="n">method</span><span class="w"> </span><span class="nf">sumAndZero</span><span class="p">(</span><span class="n">arr</span><span class="p">:</span><span class="w"> </span><span class="n">array</span><span class="o"><</span><span class="kt">int</span><span class="o">></span><span class="p">)</span><span class="w"> </span><span class="n">returns</span><span class="w"> </span><span class="p">(</span><span class="n">sum</span><span class="p">:</span><span class="w"> </span><span class="n">nat</span><span class="p">)</span> <span class="w"> </span><span class="n">requires</span><span class="w"> </span><span class="n">forall</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="p">::</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="o"><=</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="o"><</span><span class="w"> </span><span class="n">arr</span><span class="p">.</span><span class="na">Length</span><span class="w"> </span><span class="o">==></span><span class="w"> </span><span class="n">arr</span><span class="o">[</span><span class="n">i</span><span class="o">]</span><span class="w"> </span><span class="o">>=</span><span class="w"> </span><span class="mi">0</span> <span class="w"> </span><span class="n">modifies</span><span class="w"> </span><span class="n">arr</span> <span class="p">{</span> <span class="w"> </span><span class="kd">var</span><span class="w"> </span><span class="n">i</span><span class="p">:</span><span class="w"> </span><span class="kt">int</span><span class="w"> </span><span class="p">:</span><span class="o">=</span><span class="w"> </span><span class="mi">0</span><span class="p">;</span> <span class="w"> </span><span class="n">sum</span><span class="w"> </span><span class="p">:</span><span class="o">=</span><span class="w"> </span><span class="mi">0</span><span class="p">;</span> <span class="w"> </span><span class="c1">//</span> <span class="w"> </span><span class="k">while</span><span class="p">(</span><span class="n">i</span><span class="w"> </span><span class="o"><</span><span class="w"> </span><span class="n">arr</span><span class="p">.</span><span class="na">Length</span><span class="p">)</span><span class="w"> </span><span class="p">{</span> <span class="w"> </span><span class="n">sum</span><span class="w"> </span><span class="p">:</span><span class="o">=</span><span class="w"> </span><span class="n">sum</span><span class="w"> </span><span class="o">+</span><span class="w"> </span><span class="n">arr</span><span class="o">[</span><span class="n">i</span><span class="o">]</span><span class="p">;</span> <span class="w"> </span><span class="n">arr</span><span class="o">[</span><span class="n">i</span><span class="o">]</span><span class="w"> </span><span class="p">:</span><span class="o">=</span><span class="w"> </span><span class="n">arr</span><span class="o">[</span><span class="n">i</span><span class="o">]</span><span class="p">;</span> <span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="p">:</span><span class="o">=</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="o">+</span><span class="w"> </span><span class="mi">1</span><span class="p">;</span> <span class="w"> </span><span class="p">}</span> <span class="p">}</span> </pre></div> <p>This fails verification because Dafny cannot establish that <code>(sum + arr[i]) >= 0</code> holds at the assignment. From the precondition, intuitively, <code>forall i :: 0 <= i < arr.Length ==> arr[i] >= 0</code> holds in the loop since <code>arr[i] := arr[i];</code> is a <a href="/wiki/NOP_(code)" title="NOP (code)">NOP</a>. However, this assignment causes Dafny to treat <code>arr</code> as a mutable variable and drop information known about it from before the loop. To verify this program in Dafny we can either (a) remove the redundant assignment <code>arr[i] := arr[i];</code>; or (b) add the loop invariant <code>invariant forall i :: 0 <= i < arr.Length ==> arr[i] >= 0</code> </p><p>Dafny additionally employs limited <a href="/wiki/Static_program_analysis" title="Static program analysis">static analysis</a> to infer simple loop invariants where possible. In the example above, it would seem that the loop invariant <code>invariant i >= 0</code> is also required as variable <code>i</code> is mutated within the loop. Whilst the underlying logic does require such an invariant, Dafny automatically infers this and, hence, it can be omitted at the source level. </p> <div class="mw-heading mw-heading2"><h2 id="Proof_features">Proof features</h2><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Dafny&action=edit&section=4" title="Edit section: Proof features"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <p>Dafny includes features which further support its use as a <a href="/wiki/Proof_assistant" title="Proof assistant">proof assistant</a>. Although proofs of simple properties within a <code>function</code> or <code>method</code> (as shown above) are not unusual for tools of this nature, Dafny also allows the proof of properties between one <code>function</code> and another. As is common for a <a href="/wiki/Proof_assistant" title="Proof assistant">proof assistant</a>, such proofs are often <a href="/wiki/Mathematical_induction" title="Mathematical induction">inductive</a> in nature. Dafny is perhaps unusual in employing method invocation as a mechanism for applying the inductive hypothesis. The following illustrates: </p> <div class="mw-highlight mw-highlight-lang-c# mw-content-ltr" dir="ltr"><pre><span></span><span class="n">datatype</span><span class="w"> </span><span class="n">List</span><span class="w"> </span><span class="o">=</span><span class="w"> </span><span class="n">Nil</span><span class="w"> </span><span class="o">|</span><span class="w"> </span><span class="n">Link</span><span class="p">(</span><span class="n">data</span><span class="p">:</span><span class="w"> </span><span class="kt">int</span><span class="p">,</span><span class="w"> </span><span class="n">next</span><span class="p">:</span><span class="w"> </span><span class="n">List</span><span class="p">)</span> <span class="n">function</span><span class="w"> </span><span class="nf">sum</span><span class="p">(</span><span class="n">l</span><span class="p">:</span><span class="w"> </span><span class="n">List</span><span class="p">):</span><span class="w"> </span><span class="kt">int</span><span class="w"> </span><span class="p">{</span> <span class="w"> </span><span class="n">match</span><span class="w"> </span><span class="n">l</span> <span class="w"> </span><span class="k">case</span><span class="w"> </span><span class="n">Nil</span><span class="w"> </span><span class="o">=></span><span class="w"> </span><span class="m">0</span> <span class="w"> </span><span class="k">case</span><span class="w"> </span><span class="nf">Link</span><span class="p">(</span><span class="n">d</span><span class="p">,</span><span class="w"> </span><span class="n">n</span><span class="p">)</span><span class="w"> </span><span class="o">=></span><span class="w"> </span><span class="n">d</span><span class="w"> </span><span class="o">+</span><span class="w"> </span><span class="n">sum</span><span class="p">(</span><span class="n">n</span><span class="p">)</span> <span class="p">}</span> <span class="n">predicate</span><span class="w"> </span><span class="nf">isNatList</span><span class="p">(</span><span class="n">l</span><span class="p">:</span><span class="w"> </span><span class="n">List</span><span class="p">)</span><span class="w"> </span><span class="p">{</span> <span class="w"> </span><span class="n">match</span><span class="w"> </span><span class="n">l</span> <span class="w"> </span><span class="k">case</span><span class="w"> </span><span class="n">Nil</span><span class="w"> </span><span class="o">=></span><span class="w"> </span><span class="k">true</span> <span class="w"> </span><span class="k">case</span><span class="w"> </span><span class="nf">Link</span><span class="p">(</span><span class="n">d</span><span class="p">,</span><span class="w"> </span><span class="n">n</span><span class="p">)</span><span class="w"> </span><span class="o">=></span><span class="w"> </span><span class="n">d</span><span class="w"> </span><span class="o">>=</span><span class="w"> </span><span class="m">0</span><span class="w"> </span><span class="o">&&</span><span class="w"> </span><span class="n">isNatList</span><span class="p">(</span><span class="n">n</span><span class="p">)</span> <span class="p">}</span> <span class="n">lemma</span><span class="w"> </span><span class="nf">NatSumLemma</span><span class="p">(</span><span class="n">l</span><span class="p">:</span><span class="w"> </span><span class="n">List</span><span class="p">,</span><span class="w"> </span><span class="n">n</span><span class="p">:</span><span class="w"> </span><span class="kt">int</span><span class="p">)</span> <span class="w"> </span><span class="n">requires</span><span class="w"> </span><span class="nf">isNatList</span><span class="p">(</span><span class="n">l</span><span class="p">)</span><span class="w"> </span><span class="o">&&</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">==</span><span class="w"> </span><span class="n">sum</span><span class="p">(</span><span class="n">l</span><span class="p">)</span> <span class="w"> </span><span class="n">ensures</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">>=</span><span class="w"> </span><span class="m">0</span><span class="w"> </span> <span class="p">{</span> <span class="w"> </span><span class="n">match</span><span class="w"> </span><span class="n">l</span> <span class="w"> </span><span class="k">case</span><span class="w"> </span><span class="n">Nil</span><span class="w"> </span><span class="o">=></span> <span class="w"> </span><span class="c1">// Discharged Automatically</span> <span class="w"> </span><span class="k">case</span><span class="w"> </span><span class="nf">Link</span><span class="p">(</span><span class="n">data</span><span class="p">,</span><span class="w"> </span><span class="n">next</span><span class="p">)</span><span class="w"> </span><span class="o">=></span><span class="w"> </span><span class="p">{</span> <span class="w"> </span><span class="c1">// Apply Inductive Hypothesis</span> <span class="w"> </span><span class="n">NatSumLemma</span><span class="p">(</span><span class="n">next</span><span class="p">,</span><span class="w"> </span><span class="n">sum</span><span class="p">(</span><span class="n">next</span><span class="p">));</span> <span class="w"> </span><span class="c1">// Check what known by Dafny</span> <span class="w"> </span><span class="n">assert</span><span class="w"> </span><span class="n">data</span><span class="w"> </span><span class="o">>=</span><span class="w"> </span><span class="m">0</span><span class="p">;</span> <span class="w"> </span><span class="p">}</span> <span class="p">}</span> </pre></div> <p>Here, <code>NatSumLemma</code> proves a useful property <i>between</i> <code>sum()</code> and <code>isNatList()</code> (i.e. that <code>isNatList(l) ==> (sum(l) >= 0)</code>). The use of a <code>ghost method</code> for encoding <a href="/wiki/Lemma_(mathematics)" title="Lemma (mathematics)">lemmas and theorems</a> is standard in Dafny with recursion employed for induction (typically, <a href="/wiki/Structural_induction" title="Structural induction">structural induction</a>). <a href="/wiki/Proof_by_exhaustion" title="Proof by exhaustion">Case analysis</a> is performed using <code>match</code> statements and non-inductive cases are often discharged automatically. The verifier must also have complete access to the contents of a <code>function</code> or <code>predicate</code> in order to unroll them as necessary. This has implications when used in conjunction with <a href="/wiki/Access_modifiers" title="Access modifiers">access modifiers</a>. Specifically, hiding the contents of a <code>function</code> using the <code>protected</code> modifier can limit what properties can be established about it. </p> <div class="mw-heading mw-heading2"><h2 id="See_also">See also</h2><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Dafny&action=edit&section=5" title="Edit section: See also"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <ul><li><a href="/wiki/Design_by_contract" title="Design by contract">Design by contract</a></li></ul> <div class="mw-heading mw-heading2"><h2 id="References">References</h2><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Dafny&action=edit&section=6" title="Edit section: References"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <style data-mw-deduplicate="TemplateStyles:r1239543626">.mw-parser-output .reflist{margin-bottom:0.5em;list-style-type:decimal}@media screen{.mw-parser-output .reflist{font-size:90%}}.mw-parser-output .reflist .references{font-size:100%;margin-bottom:0;list-style-type:inherit}.mw-parser-output .reflist-columns-2{column-width:30em}.mw-parser-output .reflist-columns-3{column-width:25em}.mw-parser-output .reflist-columns{margin-top:0.3em}.mw-parser-output .reflist-columns ol{margin-top:0}.mw-parser-output .reflist-columns li{page-break-inside:avoid;break-inside:avoid-column}.mw-parser-output .reflist-upper-alpha{list-style-type:upper-alpha}.mw-parser-output .reflist-upper-roman{list-style-type:upper-roman}.mw-parser-output .reflist-lower-alpha{list-style-type:lower-alpha}.mw-parser-output .reflist-lower-greek{list-style-type:lower-greek}.mw-parser-output .reflist-lower-roman{list-style-type:lower-roman}</style><div class="reflist"> <div class="mw-references-wrap"><ol class="references"> <li id="cite_note-1"><span class="mw-cite-backlink"><b><a href="#cite_ref-1">^</a></b></span> <span class="reference-text"><style data-mw-deduplicate="TemplateStyles:r1238218222">.mw-parser-output cite.citation{font-style:inherit;word-wrap:break-word}.mw-parser-output .citation q{quotes:"\"""\"""'""'"}.mw-parser-output .citation:target{background-color:rgba(0,127,255,0.133)}.mw-parser-output .id-lock-free.id-lock-free a{background:url("//upload.wikimedia.org/wikipedia/commons/6/65/Lock-green.svg")right 0.1em center/9px no-repeat}.mw-parser-output .id-lock-limited.id-lock-limited a,.mw-parser-output .id-lock-registration.id-lock-registration a{background:url("//upload.wikimedia.org/wikipedia/commons/d/d6/Lock-gray-alt-2.svg")right 0.1em center/9px no-repeat}.mw-parser-output .id-lock-subscription.id-lock-subscription a{background:url("//upload.wikimedia.org/wikipedia/commons/a/aa/Lock-red-alt-2.svg")right 0.1em center/9px no-repeat}.mw-parser-output .cs1-ws-icon a{background:url("//upload.wikimedia.org/wikipedia/commons/4/4c/Wikisource-logo.svg")right 0.1em center/12px no-repeat}body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-free a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-limited a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-registration a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-subscription a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .cs1-ws-icon a{background-size:contain;padding:0 1em 0 0}.mw-parser-output .cs1-code{color:inherit;background:inherit;border:none;padding:inherit}.mw-parser-output .cs1-hidden-error{display:none;color:var(--color-error,#d33)}.mw-parser-output .cs1-visible-error{color:var(--color-error,#d33)}.mw-parser-output .cs1-maint{display:none;color:#085;margin-left:0.3em}.mw-parser-output .cs1-kern-left{padding-left:0.2em}.mw-parser-output .cs1-kern-right{padding-right:0.2em}.mw-parser-output .citation .mw-selflink{font-weight:inherit}@media screen{.mw-parser-output .cs1-format{font-size:95%}html.skin-theme-clientpref-night .mw-parser-output .cs1-maint{color:#18911f}}@media screen and (prefers-color-scheme:dark){html.skin-theme-clientpref-os .mw-parser-output .cs1-maint{color:#18911f}}</style><cite id="CITEREFSmansJacobsPiessens2009" class="citation conference cs1">Smans, Jan; Jacobs, Bart; Piessens, Frank (2009). <a rel="nofollow" class="external text" href="https://lirias.kuleuven.be/bitstream/123456789/221907/3/ecoop09.pdf"><i>Implicit Dynamic Frames: Combining Dynamic Frames and Separation Logic</i></a> <span class="cs1-format">(PDF)</span>. Proceedings of the Conference on European Conference on Object Oriented Programming. pp. <span class="nowrap">148–</span>172. <a href="/wiki/Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1007%2F978-3-642-03013-0_8">10.1007/978-3-642-03013-0_8</a>.</cite><span title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Abook&rft.genre=conference&rft.btitle=Implicit+Dynamic+Frames%3A+Combining+Dynamic+Frames+and+Separation+Logic&rft.pages=%3Cspan+class%3D%22nowrap%22%3E148-%3C%2Fspan%3E172&rft.date=2009&rft_id=info%3Adoi%2F10.1007%2F978-3-642-03013-0_8&rft.aulast=Smans&rft.aufirst=Jan&rft.au=Jacobs%2C+Bart&rft.au=Piessens%2C+Frank&rft_id=https%3A%2F%2Flirias.kuleuven.be%2Fbitstream%2F123456789%2F221907%2F3%2Fecoop09.pdf&rfr_id=info%3Asid%2Fen.wikipedia.org%3ADafny" class="Z3988"></span></span> </li> <li id="cite_note-2"><span class="mw-cite-backlink"><b><a href="#cite_ref-2">^</a></b></span> <span class="reference-text"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1238218222" /><cite id="CITEREFLeino2010" class="citation conference cs1">Leino, Rustan (2010). <i>Dafny: An Automatic Program Verifier for Functional Correctness</i>. Proceedings of the Conference on Logic for Programming, Artificial Intelligence, and Reasoning. pp. <span class="nowrap">348–</span>370. <a href="/wiki/Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1007%2F978-3-642-17511-4_20">10.1007/978-3-642-17511-4_20</a>.</cite><span title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Abook&rft.genre=conference&rft.btitle=Dafny%3A+An+Automatic+Program+Verifier+for+Functional+Correctness&rft.pages=%3Cspan+class%3D%22nowrap%22%3E348-%3C%2Fspan%3E370&rft.date=2010&rft_id=info%3Adoi%2F10.1007%2F978-3-642-17511-4_20&rft.aulast=Leino&rft.aufirst=Rustan&rfr_id=info%3Asid%2Fen.wikipedia.org%3ADafny" class="Z3988"></span></span> </li> <li id="cite_note-3"><span class="mw-cite-backlink"><b><a href="#cite_ref-3">^</a></b></span> <span class="reference-text"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1238218222" /><cite id="CITEREFLeinoMonahan2010" class="citation conference cs1">Leino, Rustan; Monahan, Rosemary (2010). <a rel="nofollow" class="external text" href="http://eprints.maynoothuniversity.ie/3840/1/RM_Dafny.pdf"><i>Dafny Meets the Verification Benchmarks Challenge</i></a> <span class="cs1-format">(PDF)</span>. International Conference on Verified Software: Theories, Tools, and Experiments. pp. <span class="nowrap">112–</span>116. <a href="/wiki/Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1007%2F978-3-642-15057-9_8">10.1007/978-3-642-15057-9_8</a>.</cite><span title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Abook&rft.genre=conference&rft.btitle=Dafny+Meets+the+Verification+Benchmarks+Challenge&rft.pages=%3Cspan+class%3D%22nowrap%22%3E112-%3C%2Fspan%3E116&rft.date=2010&rft_id=info%3Adoi%2F10.1007%2F978-3-642-15057-9_8&rft.aulast=Leino&rft.aufirst=Rustan&rft.au=Monahan%2C+Rosemary&rft_id=http%3A%2F%2Feprints.maynoothuniversity.ie%2F3840%2F1%2FRM_Dafny.pdf&rfr_id=info%3Asid%2Fen.wikipedia.org%3ADafny" class="Z3988"></span></span> </li> <li id="cite_note-4"><span class="mw-cite-backlink"><b><a href="#cite_ref-4">^</a></b></span> <span class="reference-text"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1238218222" /><cite id="CITEREFKlebanov2011" class="citation conference cs1">Klebanov, Vladimir; et al. (2011). <i>The 1st Verified Software Competition: Experience Report</i>. Proceedings of the Conference on Formal Methods. pp. <span class="nowrap">154–</span>168. <a href="/wiki/CiteSeerX_(identifier)" class="mw-redirect" title="CiteSeerX (identifier)">CiteSeerX</a> <span class="id-lock-free" title="Freely accessible"><a rel="nofollow" class="external text" href="https://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.221.6890">10.1.1.221.6890</a></span>. <a href="/wiki/Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1007%2F978-3-642-21437-0_14">10.1007/978-3-642-21437-0_14</a>.</cite><span title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Abook&rft.genre=conference&rft.btitle=The+1st+Verified+Software+Competition%3A+Experience+Report&rft.pages=%3Cspan+class%3D%22nowrap%22%3E154-%3C%2Fspan%3E168&rft.date=2011&rft_id=https%3A%2F%2Fciteseerx.ist.psu.edu%2Fviewdoc%2Fsummary%3Fdoi%3D10.1.1.221.6890%23id-name%3DCiteSeerX&rft_id=info%3Adoi%2F10.1007%2F978-3-642-21437-0_14&rft.aulast=Klebanov&rft.aufirst=Vladimir&rfr_id=info%3Asid%2Fen.wikipedia.org%3ADafny" class="Z3988"></span></span> </li> <li id="cite_note-5"><span class="mw-cite-backlink"><b><a href="#cite_ref-5">^</a></b></span> <span class="reference-text"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1238218222" /><cite id="CITEREFBormer2011" class="citation conference cs1">Bormer, Thorsten; et al. (2011). <i>The COST IC0701 Verification Competition 2011</i>. Proceedings of the Conference on Formal Verification of Object-Oriented Software. pp. <span class="nowrap">3–</span>21. <a href="/wiki/CiteSeerX_(identifier)" class="mw-redirect" title="CiteSeerX (identifier)">CiteSeerX</a> <span class="id-lock-free" title="Freely accessible"><a rel="nofollow" class="external text" href="https://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.396.6170">10.1.1.396.6170</a></span>. <a href="/wiki/Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1007%2F978-3-642-31762-0_2">10.1007/978-3-642-31762-0_2</a>.</cite><span title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Abook&rft.genre=conference&rft.btitle=The+COST+IC0701+Verification+Competition+2011&rft.pages=%3Cspan+class%3D%22nowrap%22%3E3-%3C%2Fspan%3E21&rft.date=2011&rft_id=https%3A%2F%2Fciteseerx.ist.psu.edu%2Fviewdoc%2Fsummary%3Fdoi%3D10.1.1.396.6170%23id-name%3DCiteSeerX&rft_id=info%3Adoi%2F10.1007%2F978-3-642-31762-0_2&rft.aulast=Bormer&rft.aufirst=Thorsten&rfr_id=info%3Asid%2Fen.wikipedia.org%3ADafny" class="Z3988"></span></span> </li> <li id="cite_note-6"><span class="mw-cite-backlink"><b><a href="#cite_ref-6">^</a></b></span> <span class="reference-text"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1238218222" /><cite id="CITEREFHuismanKlebanovMonahan2015" class="citation journal cs1">Huisman, Marieke; Klebanov, Vladimir; Monahan, Rosemary (2015). <a rel="nofollow" class="external text" href="http://mural.maynoothuniversity.ie/12375/1/Monahan_VerifyThis2012_2015.pdf">"VerifyThis 2012"</a> <span class="cs1-format">(PDF)</span>. <i>International Journal on Software Tools for Technology Transfer</i>. <b>17</b> (6): <span class="nowrap">647–</span>657. <a href="/wiki/Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1007%2Fs10009-015-0396-8">10.1007/s10009-015-0396-8</a>. <a href="/wiki/S2CID_(identifier)" class="mw-redirect" title="S2CID (identifier)">S2CID</a> <a rel="nofollow" class="external text" href="https://api.semanticscholar.org/CorpusID:14301377">14301377</a>.</cite><span title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Ajournal&rft.genre=article&rft.jtitle=International+Journal+on+Software+Tools+for+Technology+Transfer&rft.atitle=VerifyThis+2012&rft.volume=17&rft.issue=6&rft.pages=%3Cspan+class%3D%22nowrap%22%3E647-%3C%2Fspan%3E657&rft.date=2015&rft_id=info%3Adoi%2F10.1007%2Fs10009-015-0396-8&rft_id=https%3A%2F%2Fapi.semanticscholar.org%2FCorpusID%3A14301377%23id-name%3DS2CID&rft.aulast=Huisman&rft.aufirst=Marieke&rft.au=Klebanov%2C+Vladimir&rft.au=Monahan%2C+Rosemary&rft_id=http%3A%2F%2Fmural.maynoothuniversity.ie%2F12375%2F1%2FMonahan_VerifyThis2012_2015.pdf&rfr_id=info%3Asid%2Fen.wikipedia.org%3ADafny" class="Z3988"></span></span> </li> <li id="cite_note-7"><span class="mw-cite-backlink"><b><a href="#cite_ref-7">^</a></b></span> <span class="reference-text"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1238218222" /><cite class="citation web cs1"><a rel="nofollow" class="external text" href="https://github.com/Z3Prover/z3">"Z3 Homepage"</a>. <i><a href="/wiki/GitHub" title="GitHub">GitHub</a></i>. 2019-02-07.</cite><span title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Ajournal&rft.genre=unknown&rft.jtitle=GitHub&rft.atitle=Z3+Homepage&rft.date=2019-02-07&rft_id=https%3A%2F%2Fgithub.com%2FZ3Prover%2Fz3&rfr_id=info%3Asid%2Fen.wikipedia.org%3ADafny" class="Z3988"></span></span> </li> <li id="cite_note-8"><span class="mw-cite-backlink"><b><a href="#cite_ref-8">^</a></b></span> <span class="reference-text"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1238218222" /><cite id="CITEREFde_MouraBjørner2008" class="citation conference cs1">de Moura, Leonardo; Bjørner, Nikolaj (2008). <i>Z3: An Efficient SMT Solver</i>. Proceedings of the Conference on Tools and Algorithms for the Construction and Analysis. pp. <span class="nowrap">337–</span>340. <a href="/wiki/Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<span class="id-lock-free" title="Freely accessible"><a rel="nofollow" class="external text" href="https://doi.org/10.1007%2F978-3-540-78800-3_24">10.1007/978-3-540-78800-3_24</a></span>.</cite><span title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Abook&rft.genre=conference&rft.btitle=Z3%3A+An+Efficient+SMT+Solver&rft.pages=%3Cspan+class%3D%22nowrap%22%3E337-%3C%2Fspan%3E340&rft.date=2008&rft_id=info%3Adoi%2F10.1007%2F978-3-540-78800-3_24&rft.aulast=de+Moura&rft.aufirst=Leonardo&rft.au=Bj%C3%B8rner%2C+Nikolaj&rfr_id=info%3Asid%2Fen.wikipedia.org%3ADafny" class="Z3988"></span></span> </li> <li id="cite_note-9"><span class="mw-cite-backlink"><b><a href="#cite_ref-9">^</a></b></span> <span class="reference-text"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1238218222" /><cite class="citation web cs1"><a rel="nofollow" class="external text" href="https://dafny.org">"Dafny Programming Language"</a>. 2022-07-14.</cite><span title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Abook&rft.genre=unknown&rft.btitle=Dafny+Programming+Language&rft.date=2022-07-14&rft_id=https%3A%2F%2Fdafny.org&rfr_id=info%3Asid%2Fen.wikipedia.org%3ADafny" class="Z3988"></span></span> </li> </ol></div></div> <div class="mw-heading mw-heading2"><h2 id="Further_reading">Further reading</h2><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Dafny&action=edit&section=7" title="Edit section: Further reading"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <ul><li><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1238218222" /><cite id="CITEREFMeyerNordio2012" class="citation book cs1">Meyer, Bertrand; Nordio, Martin, eds. (2012). <i>Tools for Practical Software Verification: International Summer School, LASER 2011, Elba Island, Italy, Revised Tutorial Lectures</i>. <a href="/wiki/Springer_Science%2BBusiness_Media" title="Springer Science+Business Media">Springer</a>. <a href="/wiki/ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <a href="/wiki/Special:BookSources/978-3642357459" title="Special:BookSources/978-3642357459"><bdi>978-3642357459</bdi></a>.</cite><span title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Abook&rft.genre=book&rft.btitle=Tools+for+Practical+Software+Verification%3A+International+Summer+School%2C+LASER+2011%2C+Elba+Island%2C+Italy%2C+Revised+Tutorial+Lectures&rft.pub=Springer&rft.date=2012&rft.isbn=978-3642357459&rfr_id=info%3Asid%2Fen.wikipedia.org%3ADafny" class="Z3988"></span></li> <li><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1238218222" /><cite id="CITEREFSitnikovski2022" class="citation book cs1">Sitnikovski, Boro (2022). <i>Introducing Software Verification with Dafny Language: Proving Program Correctness</i>. Apress. <a href="/wiki/ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <a href="/wiki/Special:BookSources/978-1484279779" title="Special:BookSources/978-1484279779"><bdi>978-1484279779</bdi></a>.</cite><span title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Abook&rft.genre=book&rft.btitle=Introducing+Software+Verification+with+Dafny+Language%3A+Proving+Program+Correctness&rft.pub=Apress&rft.date=2022&rft.isbn=978-1484279779&rft.aulast=Sitnikovski&rft.aufirst=Boro&rfr_id=info%3Asid%2Fen.wikipedia.org%3ADafny" class="Z3988"></span></li></ul> <div class="mw-heading mw-heading2"><h2 id="External_links">External links</h2><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Dafny&action=edit&section=8" title="Edit section: External links"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <ul><li><a rel="nofollow" class="external text" href="https://www.microsoft.com/en-us/research/project/dafny-a-language-and-program-verifier-for-functional-correctness/">Dafny: A Language and Program Verifier for Functional Correctness - Microsoft Research</a></li> <li><a rel="nofollow" class="external text" href="https://github.com/dafny-lang/dafny">GitHub - dafny-lang/dafny: Dafny is a verification-aware programming language</a></li></ul> <div class="navbox-styles"><style data-mw-deduplicate="TemplateStyles:r1129693374">.mw-parser-output .hlist dl,.mw-parser-output .hlist ol,.mw-parser-output .hlist ul{margin:0;padding:0}.mw-parser-output .hlist dd,.mw-parser-output .hlist dt,.mw-parser-output .hlist li{margin:0;display:inline}.mw-parser-output .hlist.inline,.mw-parser-output .hlist.inline dl,.mw-parser-output .hlist.inline ol,.mw-parser-output .hlist.inline ul,.mw-parser-output .hlist dl dl,.mw-parser-output .hlist dl ol,.mw-parser-output .hlist dl ul,.mw-parser-output .hlist ol dl,.mw-parser-output .hlist ol ol,.mw-parser-output .hlist ol ul,.mw-parser-output .hlist ul dl,.mw-parser-output .hlist ul ol,.mw-parser-output .hlist ul ul{display:inline}.mw-parser-output .hlist .mw-empty-li{display:none}.mw-parser-output .hlist dt::after{content:": "}.mw-parser-output .hlist dd::after,.mw-parser-output .hlist li::after{content:" · ";font-weight:bold}.mw-parser-output .hlist dd:last-child::after,.mw-parser-output .hlist dt:last-child::after,.mw-parser-output .hlist li:last-child::after{content:none}.mw-parser-output .hlist dd dd:first-child::before,.mw-parser-output .hlist dd dt:first-child::before,.mw-parser-output .hlist dd li:first-child::before,.mw-parser-output .hlist dt dd:first-child::before,.mw-parser-output .hlist dt dt:first-child::before,.mw-parser-output .hlist dt li:first-child::before,.mw-parser-output .hlist li dd:first-child::before,.mw-parser-output .hlist li dt:first-child::before,.mw-parser-output .hlist li li:first-child::before{content:" (";font-weight:normal}.mw-parser-output .hlist dd dd:last-child::after,.mw-parser-output .hlist dd dt:last-child::after,.mw-parser-output .hlist dd li:last-child::after,.mw-parser-output .hlist dt dd:last-child::after,.mw-parser-output .hlist dt dt:last-child::after,.mw-parser-output .hlist dt li:last-child::after,.mw-parser-output .hlist li dd:last-child::after,.mw-parser-output .hlist li dt:last-child::after,.mw-parser-output .hlist li li:last-child::after{content:")";font-weight:normal}.mw-parser-output .hlist ol{counter-reset:listitem}.mw-parser-output .hlist ol>li{counter-increment:listitem}.mw-parser-output .hlist ol>li::before{content:" "counter(listitem)"\a0 "}.mw-parser-output .hlist dd ol>li:first-child::before,.mw-parser-output .hlist dt ol>li:first-child::before,.mw-parser-output .hlist li ol>li:first-child::before{content:" ("counter(listitem)"\a0 "}</style><style data-mw-deduplicate="TemplateStyles:r1236075235">.mw-parser-output .navbox{box-sizing:border-box;border:1px solid #a2a9b1;width:100%;clear:both;font-size:88%;text-align:center;padding:1px;margin:1em auto 0}.mw-parser-output .navbox .navbox{margin-top:0}.mw-parser-output .navbox+.navbox,.mw-parser-output .navbox+.navbox-styles+.navbox{margin-top:-1px}.mw-parser-output .navbox-inner,.mw-parser-output .navbox-subgroup{width:100%}.mw-parser-output .navbox-group,.mw-parser-output .navbox-title,.mw-parser-output .navbox-abovebelow{padding:0.25em 1em;line-height:1.5em;text-align:center}.mw-parser-output .navbox-group{white-space:nowrap;text-align:right}.mw-parser-output .navbox,.mw-parser-output .navbox-subgroup{background-color:#fdfdfd}.mw-parser-output .navbox-list{line-height:1.5em;border-color:#fdfdfd}.mw-parser-output .navbox-list-with-group{text-align:left;border-left-width:2px;border-left-style:solid}.mw-parser-output tr+tr>.navbox-abovebelow,.mw-parser-output tr+tr>.navbox-group,.mw-parser-output tr+tr>.navbox-image,.mw-parser-output tr+tr>.navbox-list{border-top:2px solid #fdfdfd}.mw-parser-output .navbox-title{background-color:#ccf}.mw-parser-output .navbox-abovebelow,.mw-parser-output .navbox-group,.mw-parser-output .navbox-subgroup .navbox-title{background-color:#ddf}.mw-parser-output .navbox-subgroup .navbox-group,.mw-parser-output .navbox-subgroup .navbox-abovebelow{background-color:#e6e6ff}.mw-parser-output .navbox-even{background-color:#f7f7f7}.mw-parser-output .navbox-odd{background-color:transparent}.mw-parser-output .navbox .hlist td dl,.mw-parser-output .navbox .hlist td ol,.mw-parser-output .navbox .hlist td ul,.mw-parser-output .navbox td.hlist dl,.mw-parser-output .navbox td.hlist ol,.mw-parser-output .navbox td.hlist ul{padding:0.125em 0}.mw-parser-output .navbox .navbar{display:block;font-size:100%}.mw-parser-output .navbox-title .navbar{float:left;text-align:left;margin-right:0.5em}body.skin--responsive .mw-parser-output .navbox-image img{max-width:none!important}@media print{body.ns-0 .mw-parser-output .navbox{display:none!important}}</style></div><div role="navigation" class="navbox" aria-labelledby="Microsoft_free_and_open-source_software_(FOSS)290" style="padding:3px"><table class="nowraplinks mw-collapsible autocollapse navbox-inner" style="border-spacing:0;background:transparent;color:inherit"><tbody><tr><th scope="col" class="navbox-title" colspan="2"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1129693374" /><style data-mw-deduplicate="TemplateStyles:r1239400231">.mw-parser-output .navbar{display:inline;font-size:88%;font-weight:normal}.mw-parser-output .navbar-collapse{float:left;text-align:left}.mw-parser-output .navbar-boxtext{word-spacing:0}.mw-parser-output .navbar ul{display:inline-block;white-space:nowrap;line-height:inherit}.mw-parser-output .navbar-brackets::before{margin-right:-0.125em;content:"[ "}.mw-parser-output .navbar-brackets::after{margin-left:-0.125em;content:" ]"}.mw-parser-output .navbar li{word-spacing:-0.125em}.mw-parser-output .navbar a>span,.mw-parser-output .navbar a>abbr{text-decoration:inherit}.mw-parser-output .navbar-mini abbr{font-variant:small-caps;border-bottom:none;text-decoration:none;cursor:inherit}.mw-parser-output .navbar-ct-full{font-size:114%;margin:0 7em}.mw-parser-output .navbar-ct-mini{font-size:114%;margin:0 4em}html.skin-theme-clientpref-night .mw-parser-output .navbar li a abbr{color:var(--color-base)!important}@media(prefers-color-scheme:dark){html.skin-theme-clientpref-os .mw-parser-output .navbar li a abbr{color:var(--color-base)!important}}@media print{.mw-parser-output .navbar{display:none!important}}</style><div class="navbar plainlinks hlist navbar-mini"><ul><li class="nv-view"><a href="/wiki/Template:Microsoft_FOSS" title="Template:Microsoft FOSS"><abbr title="View this template">v</abbr></a></li><li class="nv-talk"><a href="/wiki/Template_talk:Microsoft_FOSS" title="Template talk:Microsoft FOSS"><abbr title="Discuss this template">t</abbr></a></li><li class="nv-edit"><a href="/wiki/Special:EditPage/Template:Microsoft_FOSS" title="Special:EditPage/Template:Microsoft FOSS"><abbr title="Edit this template">e</abbr></a></li></ul></div><div id="Microsoft_free_and_open-source_software_(FOSS)290" style="font-size:114%;margin:0 4em"><a href="/wiki/Microsoft" title="Microsoft">Microsoft</a> <a href="/wiki/Free_and_open-source_software" title="Free and open-source software">free and open-source software (FOSS)</a></div></th></tr><tr><th scope="row" class="navbox-group" style="width:1%">Overview</th><td class="navbox-list-with-group navbox-list navbox-odd hlist" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Microsoft_and_open_source" title="Microsoft and open source">Microsoft and open source</a></li> <li><a href="/wiki/Shared_Source_Initiative" title="Shared Source Initiative">Shared Source Initiative</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Software</th><td class="navbox-list-with-group navbox-list navbox-odd hlist" style="width:100%;padding:0"><div style="padding:0 0.25em"></div><table class="nowraplinks navbox-subgroup" style="border-spacing:0"><tbody><tr><th scope="row" class="navbox-group" style="width:1%">Applications</th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/3D_Movie_Maker" title="3D Movie Maker">3D Movie Maker</a></li> <li><a href="/wiki/Atom_(text_editor)" title="Atom (text editor)">Atom</a></li> <li><a href="/wiki/Conference_XP" title="Conference XP">Conference XP</a></li> <li><a href="/wiki/Family.Show" title="Family.Show">Family.Show</a></li> <li><a href="/wiki/File_Manager_(Windows)" class="mw-redirect" title="File Manager (Windows)">File Manager</a></li> <li><a href="/wiki/Open_Live_Writer" title="Open Live Writer">Open Live Writer</a></li> <li><a href="/wiki/Microsoft_PowerToys" title="Microsoft PowerToys">Microsoft PowerToys</a></li> <li><a href="/wiki/Windows_Terminal" title="Windows Terminal">Terminal</a></li> <li><a href="/wiki/Windows_Calculator" title="Windows Calculator">Windows Calculator</a></li> <li><a href="/wiki/Windows_Console" title="Windows Console">Windows Console</a></li> <li><a href="/wiki/Windows_Package_Manager" title="Windows Package Manager">Windows Package Manager</a></li> <li><a href="/wiki/WorldWide_Telescope" title="WorldWide Telescope">WorldWide Telescope</a></li> <li><a href="/wiki/XML_Notepad" title="XML Notepad">XML Notepad</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Video games</th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Allegiance_(video_game)" title="Allegiance (video game)">Allegiance</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Programming<br />languages</th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Bosque_(programming_language)" title="Bosque (programming language)">Bosque</a></li> <li><a href="/wiki/C_Sharp_(programming_language)" title="C Sharp (programming language)">C#</a></li> <li><a class="mw-selflink selflink">Dafny</a></li> <li><a href="/wiki/F_Sharp_(programming_language)" title="F Sharp (programming language)">F#</a></li> <li><a href="/wiki/F*_(programming_language)" title="F* (programming language)">F*</a></li> <li><a href="/wiki/GW-BASIC" title="GW-BASIC">GW-BASIC</a></li> <li><a href="/wiki/IronPython" title="IronPython">IronPython</a></li> <li><a href="/wiki/IronRuby" title="IronRuby">IronRuby</a></li> <li><a href="/wiki/Lean_(proof_assistant)" title="Lean (proof assistant)">Lean</a></li> <li><a href="/wiki/P_(programming_language)" title="P (programming language)">P</a></li> <li><a href="/wiki/Microsoft_Power_Fx" title="Microsoft Power Fx">Power Fx</a></li> <li><a href="/wiki/PowerShell" title="PowerShell">PowerShell</a></li> <li><a href="/wiki/Project_Verona" title="Project Verona">Project Verona</a></li> <li><a href="/wiki/Q_Sharp" title="Q Sharp">Q#</a></li> <li><a href="/wiki/Microsoft_Small_Basic" title="Microsoft Small Basic">Small Basic Online</a></li> <li><a href="/wiki/TypeScript" title="TypeScript">TypeScript</a></li> <li><a href="/wiki/Visual_Basic_.NET" class="mw-redirect" title="Visual Basic .NET">Visual Basic</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Frameworks,<br />development tools</th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/.NET" title=".NET">.NET</a></li> <li><a href="/wiki/.NET_Framework" title=".NET Framework">.NET Framework</a></li> <li><a href="/wiki/.NET_Gadgeteer" title=".NET Gadgeteer">.NET Gadgeteer</a></li> <li><a href="/wiki/.NET_MAUI" class="mw-redirect" title=".NET MAUI">.NET MAUI</a></li> <li><a href="/wiki/.NET_Micro_Framework" title=".NET Micro Framework">.NET Micro Framework</a></li> <li><a href="/wiki/AirSim" title="AirSim">AirSim</a></li> <li><a href="/wiki/ASP.NET" title="ASP.NET">ASP.NET</a></li> <li><a href="/wiki/ASP.NET_AJAX" title="ASP.NET AJAX">ASP.NET AJAX</a></li> <li><a href="/wiki/ASP.NET_Core" title="ASP.NET Core">ASP.NET Core</a></li> <li><a href="/wiki/ASP.NET_MVC" title="ASP.NET MVC">ASP.NET MVC</a></li> <li><a href="/wiki/ASP.NET_Razor" title="ASP.NET Razor">ASP.NET Razor</a></li> <li><a href="/wiki/ASP.NET_Web_Forms" title="ASP.NET Web Forms">ASP.NET Web Forms</a></li> <li><a href="/wiki/Avalonia_(software_framework)" title="Avalonia (software framework)">Avalonia</a></li> <li><a href="/wiki/Babylon.js" title="Babylon.js">Babylon.js</a></li> <li><a href="/wiki/BitFunnel" title="BitFunnel">BitFunnel</a></li> <li><a href="/wiki/Blazor" title="Blazor">Blazor</a></li> <li><a href="/wiki/C%2B%2B/WinRT" title="C++/WinRT">C++/WinRT</a></li> <li><a href="/wiki/Confidential_Consortium_Framework" title="Confidential Consortium Framework">CCF</a></li> <li><a href="/wiki/Chakra_(JavaScript_engine)" title="Chakra (JavaScript engine)">ChakraCore</a></li> <li><a href="/wiki/CLR_Profiler" title="CLR Profiler">CLR Profiler</a></li> <li><a href="/wiki/Dapr" title="Dapr">Dapr</a></li> <li><a href="/wiki/DeepSpeed" title="DeepSpeed">DeepSpeed</a></li> <li><a href="/wiki/DiskSpd" title="DiskSpd">DiskSpd</a></li> <li><a href="/wiki/Dryad_(programming)" title="Dryad (programming)">Dryad</a></li> <li><a href="/wiki/Dynamic_Language_Runtime" title="Dynamic Language Runtime">Dynamic Language Runtime</a></li> <li><a href="/wiki/EBPF_on_Windows" class="mw-redirect" title="EBPF on Windows">eBPF on Windows</a></li> <li><a href="/wiki/Electron_(software_framework)" title="Electron (software framework)">Electron</a></li> <li><a href="/wiki/Entity_Framework" title="Entity Framework">Entity Framework</a></li> <li><a href="/wiki/Fluent_Design_System" title="Fluent Design System">Fluent Design System</a></li> <li><a href="/wiki/Fluid_Framework" title="Fluid Framework">Fluid Framework</a></li> <li><a href="/wiki/Infer.NET" title="Infer.NET">Infer.NET</a></li> <li><a href="/wiki/LightGBM" title="LightGBM">LightGBM</a></li> <li><a href="/wiki/Managed_Extensibility_Framework" title="Managed Extensibility Framework">Managed Extensibility Framework</a></li> <li><a href="/wiki/Microsoft_Automatic_Graph_Layout" title="Microsoft Automatic Graph Layout">Microsoft Automatic Graph Layout</a></li> <li><a href="/wiki/Microsoft_C%2B%2B_Standard_Library" class="mw-redirect" title="Microsoft C++ Standard Library">Microsoft C++ Standard Library</a></li> <li><a href="/wiki/Microsoft_Cognitive_Toolkit" title="Microsoft Cognitive Toolkit">Microsoft Cognitive Toolkit</a></li> <li><a href="/wiki/Metro_(design_language)" title="Metro (design language)">Microsoft Design Language</a></li> <li><a href="/wiki/Microsoft_Detours" title="Microsoft Detours">Microsoft Detours</a></li> <li><a href="/wiki/Microsoft_Enterprise_Library" title="Microsoft Enterprise Library">Microsoft Enterprise Library</a></li> <li><a href="/wiki/Microsoft_SEAL" title="Microsoft SEAL">Microsoft SEAL</a></li> <li><a href="/wiki/Mimalloc" title="Mimalloc">mimalloc</a></li> <li><a href="/wiki/Mixed_Reality_Toolkit" title="Mixed Reality Toolkit">Mixed Reality Toolkit</a></li> <li><a href="/wiki/ML.NET" title="ML.NET">ML.NET</a></li> <li><a href="/wiki/Mod_mono" title="Mod mono">mod_mono</a></li> <li><a href="/wiki/Mono_(software)" title="Mono (software)">Mono</a></li> <li><a href="/wiki/MonoDevelop" title="MonoDevelop">MonoDevelop</a></li> <li><a href="/wiki/MSBuild" title="MSBuild">MSBuild</a></li> <li><a href="/wiki/MsQuic" title="MsQuic">MsQuic</a></li> <li><a href="/wiki/Neural_Network_Intelligence" title="Neural Network Intelligence">Neural Network Intelligence</a></li> <li><a href="/wiki/Npm" title="Npm">npm</a></li> <li><a href="/wiki/NuGet" title="NuGet">NuGet</a></li> <li><a href="/wiki/OneFuzz" title="OneFuzz">OneFuzz</a></li> <li><a href="/wiki/Open_Management_Infrastructure" title="Open Management Infrastructure">Open Management Infrastructure</a></li> <li><a href="/wiki/Open_Neural_Network_Exchange" title="Open Neural Network Exchange">Open Neural Network Exchange</a></li> <li><a href="/wiki/Open_Service_Mesh" title="Open Service Mesh">Open Service Mesh</a></li> <li><a href="/wiki/Open_XML_SDK" class="mw-redirect" title="Open XML SDK">Open XML SDK</a></li> <li><a href="/wiki/Orleans_(software_framework)" title="Orleans (software framework)">Orleans</a></li> <li><a href="/wiki/Playwright_(software)" title="Playwright (software)">Playwright</a></li> <li><a href="/wiki/ProcDump" title="ProcDump">ProcDump</a></li> <li><a href="/wiki/Process_Monitor" title="Process Monitor">ProcMon</a></li> <li><a href="/wiki/Python_Tools_for_Visual_Studio" title="Python Tools for Visual Studio">Python Tools for Visual Studio</a></li> <li><a href="/wiki/R_Tools_for_Visual_Studio" title="R Tools for Visual Studio">R Tools for Visual Studio</a></li> <li><a href="/wiki/RecursiveExtractor" class="mw-redirect" title="RecursiveExtractor">RecursiveExtractor</a></li> <li><a href="/wiki/Roslyn_(compiler)" title="Roslyn (compiler)">Roslyn</a></li> <li><a href="/wiki/Sandcastle_(software)" title="Sandcastle (software)">Sandcastle</a></li> <li><a href="/wiki/SignalR" title="SignalR">SignalR</a></li> <li><a href="/wiki/StyleCop" title="StyleCop">StyleCop</a></li> <li><a href="/wiki/SVNBridge" title="SVNBridge">SVNBridge</a></li> <li><a href="/wiki/T2_Temporal_Prover" title="T2 Temporal Prover">T2 Temporal Prover</a></li> <li><a href="/wiki/Text_Template_Transformation_Toolkit" title="Text Template Transformation Toolkit">Text Template Transformation Toolkit</a></li> <li><a href="/wiki/TLA%2B_Toolbox" class="mw-redirect" title="TLA+ Toolbox">TLA+ Toolbox</a></li> <li><a href="/wiki/U-Prove" title="U-Prove">U-Prove</a></li> <li><a href="/wiki/Vcpkg" title="Vcpkg">vcpkg</a></li> <li><a href="/wiki/Virtual_File_System_for_Git" title="Virtual File System for Git">Virtual File System for Git</a></li> <li><a href="/wiki/Voldemort_(distributed_data_store)" title="Voldemort (distributed data store)">Voldemort</a></li> <li><a href="/wiki/VoTT" title="VoTT">VoTT</a></li> <li><a href="/wiki/Vowpal_Wabbit" title="Vowpal Wabbit">Vowpal Wabbit</a></li> <li><a href="/wiki/Windows_App_SDK" title="Windows App SDK">Windows App SDK</a></li> <li><a href="/wiki/Windows_Communication_Foundation" title="Windows Communication Foundation">Windows Communication Foundation</a></li> <li><a href="/wiki/Windows_Driver_Frameworks" title="Windows Driver Frameworks">Windows Driver Frameworks</a> <ul><li><a href="/wiki/Kernel-Mode_Driver_Framework" title="Kernel-Mode Driver Framework">KMDF</a></li> <li><a href="/wiki/User-Mode_Driver_Framework" title="User-Mode Driver Framework">UMDF</a></li></ul></li> <li><a href="/wiki/Windows_Forms" title="Windows Forms">Windows Forms</a></li> <li><a href="/wiki/Windows_Presentation_Foundation" title="Windows Presentation Foundation">Windows Presentation Foundation</a></li> <li><a href="/wiki/Windows_Template_Library" title="Windows Template Library">Windows Template Library</a></li> <li><a href="/wiki/Windows_UI_Library" title="Windows UI Library">Windows UI Library</a></li> <li><a href="/wiki/WinJS" title="WinJS">WinJS</a></li> <li><a href="/wiki/WinObjC" class="mw-redirect" title="WinObjC">WinObjC</a></li> <li><a href="/wiki/WiX" title="WiX">WiX</a></li> <li><a href="/wiki/XDP_for_Windows" class="mw-redirect" title="XDP for Windows">XDP for Windows</a></li> <li><a href="/wiki/XSP_(software)" title="XSP (software)">XSP</a></li> <li><a href="/wiki/XUnit.net" title="XUnit.net">xUnit.net</a></li> <li><a href="/wiki/Z3_Theorem_Prover" title="Z3 Theorem Prover">Z3 Theorem Prover</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Operating systems</th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/MS-DOS" title="MS-DOS">MS-DOS</a> (v1.25, v2.0 & v4.0)</li> <li><a href="/wiki/Barrelfish_(operating_system)" title="Barrelfish (operating system)">Barrelfish</a></li> <li><a href="/wiki/SONiC_(operating_system)" title="SONiC (operating system)">SONiC</a></li> <li><a href="/wiki/Azure_Linux" title="Azure Linux">Azure Linux</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Other</th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/ChronoZoom" title="ChronoZoom">ChronoZoom</a></li> <li><a href="/wiki/Extensible_Storage_Engine" title="Extensible Storage Engine">Extensible Storage Engine</a></li> <li><a href="/wiki/FlexWiki" class="mw-redirect" title="FlexWiki">FlexWiki</a></li> <li><a href="/wiki/FourQ" title="FourQ">FourQ</a></li> <li><a href="/wiki/Gollum_(software)" title="Gollum (software)">Gollum</a></li> <li><a href="/wiki/Project_Mu" class="mw-redirect" title="Project Mu">Project Mu</a></li> <li><a href="/wiki/ReactiveX" title="ReactiveX">ReactiveX</a></li> <li><a href="/wiki/SILK" title="SILK">SILK</a></li> <li><a href="/wiki/TLAPS" class="mw-redirect" title="TLAPS">TLAPS</a></li> <li><a href="/wiki/TPM_2.0_Reference_Implementation" class="mw-redirect" title="TPM 2.0 Reference Implementation">TPM 2.0 Reference Implementation</a></li> <li><a href="/wiki/WikiBhasha" title="WikiBhasha">WikiBhasha</a></li></ul> </div></td></tr></tbody></table><div></div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="/wiki/Open-source_license" title="Open-source license">Licenses</a></th><td class="navbox-list-with-group navbox-list navbox-even hlist" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Microsoft_Public_License" class="mw-redirect" title="Microsoft Public License">Microsoft Public License</a></li> <li><a href="/wiki/Microsoft_Reciprocal_License" class="mw-redirect" title="Microsoft Reciprocal License">Microsoft Reciprocal License</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="/wiki/Forge_(software)" title="Forge (software)">Forges</a></th><td class="navbox-list-with-group navbox-list navbox-odd hlist" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/CodePlex" title="CodePlex">CodePlex</a></li> <li><a href="/wiki/GitHub" title="GitHub">GitHub</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Related</th><td class="navbox-list-with-group navbox-list navbox-even hlist" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/.NET_Foundation" title=".NET Foundation">.NET Foundation</a></li> <li><a href="/wiki/F_Sharp_Software_Foundation" title="F Sharp Software Foundation">F# Software Foundation</a></li> <li><a href="/wiki/Microsoft_Open_Specification_Promise" title="Microsoft Open Specification Promise">Microsoft Open Specification Promise</a></li> <li><a href="/wiki/Open_Letter_to_Hobbyists" class="mw-redirect" title="Open Letter to Hobbyists">Open Letter to Hobbyists</a></li> <li><a href="/wiki/Open_Source_Security_Foundation" title="Open Source Security Foundation">Open Source Security Foundation</a></li> <li><a href="/wiki/Outercurve_Foundation" title="Outercurve Foundation">Outercurve Foundation</a></li></ul> </div></td></tr><tr><td class="navbox-abovebelow" colspan="2"><div><span class="noviewer" typeof="mw:File"><span title="Category"><img alt="" src="//upload.wikimedia.org/wikipedia/en/thumb/9/96/Symbol_category_class.svg/16px-Symbol_category_class.svg.png" decoding="async" width="16" height="16" class="mw-file-element" srcset="//upload.wikimedia.org/wikipedia/en/thumb/9/96/Symbol_category_class.svg/23px-Symbol_category_class.svg.png 1.5x, //upload.wikimedia.org/wikipedia/en/thumb/9/96/Symbol_category_class.svg/31px-Symbol_category_class.svg.png 2x" data-file-width="180" data-file-height="185" /></span></span> <a href="/wiki/Category:Microsoft_free_software" title="Category:Microsoft free software">Category</a></div></td></tr></tbody></table></div> <div class="navbox-styles"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1129693374" /><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1236075235" /></div><div role="navigation" class="navbox" aria-labelledby="Microsoft_development_tools271" style="padding:3px"><table class="nowraplinks mw-collapsible autocollapse navbox-inner" style="border-spacing:0;background:transparent;color:inherit"><tbody><tr><th scope="col" class="navbox-title" colspan="2"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1129693374" /><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1239400231" /><div class="navbar plainlinks hlist navbar-mini"><ul><li class="nv-view"><a href="/wiki/Template:Microsoft_development_tools" title="Template:Microsoft development tools"><abbr title="View this template">v</abbr></a></li><li class="nv-talk"><a href="/wiki/Template_talk:Microsoft_development_tools" title="Template talk:Microsoft development tools"><abbr title="Discuss this template">t</abbr></a></li><li class="nv-edit"><a href="/wiki/Special:EditPage/Template:Microsoft_development_tools" title="Special:EditPage/Template:Microsoft development tools"><abbr title="Edit this template">e</abbr></a></li></ul></div><div id="Microsoft_development_tools271" style="font-size:114%;margin:0 4em">Microsoft development tools</div></th></tr><tr><th scope="row" class="navbox-group" style="width:1%">Development<br />environments</th><td class="navbox-list-with-group navbox-list navbox-odd hlist" style="width:100%;padding:0"><div style="padding:0 0.25em"></div><table class="nowraplinks navbox-subgroup" style="border-spacing:0"><tbody><tr><th scope="row" class="navbox-group" style="width:1%"><a href="/wiki/Microsoft_Visual_Studio" class="mw-redirect" title="Microsoft Visual Studio">Visual Studio</a></th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Visual_Studio_Code" title="Visual Studio Code">Code</a></li> <li><a href="/wiki/Microsoft_Visual_Studio_Express" title="Microsoft Visual Studio Express">Express</a></li> <li><a href="/wiki/VSTS_Profiler" title="VSTS Profiler">Team System Profiler</a></li> <li><a href="/wiki/Visual_Studio_Tools_for_Applications" title="Visual Studio Tools for Applications">Tools for Applications</a></li> <li><a href="/wiki/Visual_Studio_Tools_for_Office" title="Visual Studio Tools for Office">Tools for Office</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Others</th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Microsoft_Blend" title="Microsoft Blend">Blend</a></li> <li><a href="/wiki/Microsoft_Expression_Web" title="Microsoft Expression Web">Expression Web</a></li> <li><a href="/wiki/FxCop" title="FxCop">FxCop</a></li> <li><a href="/wiki/GW-BASIC" title="GW-BASIC">GW-BASIC</a></li> <li><a href="/wiki/Microsoft_MACRO-80" title="Microsoft MACRO-80">MACRO-80</a></li> <li><a href="/wiki/Microsoft_Macro_Assembler" title="Microsoft Macro Assembler">Macro Assembler</a></li> <li><a href="/wiki/MSBuild" title="MSBuild">MSBuild</a></li> <li><a href="/wiki/Microsoft_Pascal" title="Microsoft Pascal">Pascal</a></li> <li><a href="/wiki/QuickBASIC" title="QuickBASIC">QuickBASIC</a> <ul><li><a href="/wiki/QBasic" title="QBasic">QBasic</a></li></ul></li> <li><a href="/wiki/QuickC" title="QuickC">QuickC</a></li> <li><a href="/wiki/Microsoft_Robotics_Developer_Studio" title="Microsoft Robotics Developer Studio">Robotics Developer Studio</a></li> <li><a href="/wiki/Roslyn_(compiler)" title="Roslyn (compiler)">Roslyn</a></li> <li><a href="/wiki/Microsoft_SharePoint_Designer" title="Microsoft SharePoint Designer">SharePoint Designer</a> <ul><li><a href="/wiki/Microsoft_FrontPage" title="Microsoft FrontPage">FrontPage</a></li></ul></li> <li><a href="/wiki/Microsoft_Small_Basic" title="Microsoft Small Basic">Small Basic</a></li> <li><a href="/wiki/Microsoft_WebMatrix" title="Microsoft WebMatrix">WebMatrix</a></li> <li><a href="/wiki/Windows_App_SDK" title="Windows App SDK">Windows App SDK</a></li> <li><a href="/wiki/Windows_App_Studio" title="Windows App Studio">Windows App Studio</a></li> <li><a href="/wiki/Microsoft_Windows_SDK" title="Microsoft Windows SDK">Windows SDK</a> <ul><li><a href="/wiki/CLR_Profiler" title="CLR Profiler">CLR Profiler</a></li> <li><a href="/wiki/ILAsm" title="ILAsm">ILAsm</a></li> <li><a href="/wiki/Native_Image_Generator" title="Native Image Generator">Native Image Generator</a></li> <li><a href="/wiki/WinDiff" title="WinDiff">WinDiff</a></li> <li><a href="/wiki/XAMLPad" class="mw-redirect" title="XAMLPad">XAMLPad</a></li></ul></li></ul> </div></td></tr></tbody></table><div></div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Languages</th><td class="navbox-list-with-group navbox-list navbox-odd hlist" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Microsoft_Dynamics_AX" class="mw-redirect" title="Microsoft Dynamics AX">Dynamics AX</a></li> <li><a href="/wiki/Microsoft_BASIC" title="Microsoft BASIC">BASIC</a></li> <li>Visual Basic <ul><li><a href="/wiki/Visual_Basic_(classic)" title="Visual Basic (classic)">legacy</a></li> <li><a href="/wiki/Visual_Basic_.NET" class="mw-redirect" title="Visual Basic .NET">VB.NET</a></li> <li><a href="/wiki/Visual_Basic_for_Applications" title="Visual Basic for Applications">VBA</a></li> <li><a href="/wiki/VBScript" title="VBScript">VBScript</a></li></ul></li> <li><a href="/wiki/Bosque_(programming_language)" title="Bosque (programming language)">Bosque</a></li> <li><a href="/wiki/Microsoft_Visual_C%2B%2B" title="Microsoft Visual C++">Visual C++</a> <ul><li><a href="/wiki/C%2B%2B/CX" title="C++/CX">C++/CX</a></li> <li><a href="/wiki/C%2B%2B/CLI" title="C++/CLI">C++/CLI</a></li> <li><a href="/wiki/Managed_Extensions_for_C%2B%2B" title="Managed Extensions for C++">Managed C++</a></li> <li><a href="/wiki/C%2B%2B/WinRT" title="C++/WinRT">C++/WinRT</a></li></ul></li> <li><a href="/wiki/C_Sharp_(programming_language)" title="C Sharp (programming language)">C#</a></li> <li><a href="/wiki/C/AL" title="C/AL">C/AL</a></li> <li><a class="mw-selflink selflink">Dafny</a></li> <li><a href="/wiki/Dexterity_(programming_language)" title="Dexterity (programming language)">Dexterity</a></li> <li><a href="/wiki/F_Sharp_(programming_language)" title="F Sharp (programming language)">F#</a></li> <li><a href="/wiki/F*_(programming_language)" title="F* (programming language)">F*</a></li> <li><a href="/wiki/Visual_FoxPro" title="Visual FoxPro">Visual FoxPro</a></li> <li><a href="/wiki/Java_(programming_language)" title="Java (programming language)">Java</a> <ul><li><a href="/wiki/Visual_J%2B%2B" title="Visual J++">J++</a></li> <li><a href="/wiki/Visual_J_Sharp" title="Visual J Sharp">J#</a></li></ul></li> <li><a href="/wiki/JavaScript" title="JavaScript">JavaScript</a> <ul><li><a href="/wiki/TypeScript" title="TypeScript">TypeScript</a></li> <li><a href="/wiki/JScript" title="JScript">JScript</a></li></ul></li> <li><a href="/wiki/IronPython" title="IronPython">IronPython</a></li> <li><a href="/wiki/IronRuby" title="IronRuby">IronRuby</a></li> <li><a href="/wiki/Lean_(proof_assistant)" title="Lean (proof assistant)">Lean</a></li> <li><a href="/wiki/P_(programming_language)" title="P (programming language)">P</a></li> <li><a href="/wiki/Microsoft_Power_Fx" title="Microsoft Power Fx">Power Fx</a></li> <li><a href="/wiki/PowerShell" title="PowerShell">PowerShell</a></li> <li><a href="/wiki/Project_Verona" title="Project Verona">Project Verona</a></li> <li><a href="/wiki/Q_Sharp" title="Q Sharp">Q#</a></li> <li><a href="/wiki/Microsoft_Small_Basic" title="Microsoft Small Basic">Small Basic</a></li> <li><a href="/wiki/Microsoft_Visual_Programming_Language" title="Microsoft Visual Programming Language">VPL</a></li> <li><a href="/wiki/Extensible_Application_Markup_Language" title="Extensible Application Markup Language">XAML</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">APIs and<br />frameworks</th><td class="navbox-list-with-group navbox-list navbox-odd hlist" style="width:100%;padding:0"><div style="padding:0 0.25em"></div><table class="nowraplinks navbox-subgroup" style="border-spacing:0"><tbody><tr><th scope="row" class="navbox-group" style="width:1%;font-weight:normal;">Native</th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Windows_API" title="Windows API">Windows API</a></li> <li><a href="/wiki/Microsoft_Silverlight" title="Microsoft Silverlight">Silverlight</a></li> <li><a href="/wiki/Microsoft_XNA" title="Microsoft XNA">XNA</a></li> <li><a href="/wiki/DirectX" title="DirectX">DirectX</a> <ul><li><a href="/wiki/Managed_DirectX" title="Managed DirectX">Managed DirectX</a></li></ul></li> <li><a href="/wiki/Universal_Windows_Platform" title="Universal Windows Platform">UWP</a></li> <li><a href="/wiki/Xbox_Development_Kit" title="Xbox Development Kit">Xbox Development Kit</a></li> <li><a href="/wiki/Windows_Installer" title="Windows Installer">Windows Installer</a></li> <li><a href="/wiki/WinUI" class="mw-redirect" title="WinUI">WinUI</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%;font-weight:normal;"><a href="/wiki/.NET" title=".NET">.NET</a></th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/ASP.NET" title="ASP.NET">ASP.NET</a> <ul><li><a href="/wiki/ASP.NET_Core" title="ASP.NET Core">Core</a></li> <li><a href="/wiki/ASP.NET_AJAX" title="ASP.NET AJAX">AJAX</a></li> <li><a href="/wiki/ASP.NET_Dynamic_Data" title="ASP.NET Dynamic Data">Dynamic Data</a></li> <li><a href="/wiki/ASP.NET_MVC" title="ASP.NET MVC">MVC</a></li> <li><a href="/wiki/ASP.NET_Razor" title="ASP.NET Razor">Razor</a></li> <li><a href="/wiki/ASP.NET_Web_Forms" title="ASP.NET Web Forms">Web Forms</a></li></ul></li> <li><a href="/wiki/ADO.NET" title="ADO.NET">ADO.NET</a> <ul><li><a href="/wiki/Entity_Framework" title="Entity Framework">Entity Framework</a></li></ul></li> <li><a href="/wiki/.NET_MAUI" class="mw-redirect" title=".NET MAUI">MAUI</a></li> <li><a href="/wiki/Windows_CardSpace" title="Windows CardSpace">CardSpace</a></li> <li><a href="/wiki/Windows_Communication_Foundation" title="Windows Communication Foundation">Communication Foundation</a></li> <li><a href="/wiki/Windows_Identity_Foundation" title="Windows Identity Foundation">Identity Foundation</a></li> <li><a href="/wiki/Language_Integrated_Query" title="Language Integrated Query">LINQ</a></li> <li><a href="/wiki/Windows_Presentation_Foundation" title="Windows Presentation Foundation">Presentation Foundation</a></li> <li><a href="/wiki/Windows_Workflow_Foundation" title="Windows Workflow Foundation">Workflow Foundation</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%;font-weight:normal;"><a href="/wiki/Device_driver" title="Device driver">Device drivers</a></th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Windows_Driver_Kit" title="Windows Driver Kit">WDK</a></li> <li><a href="/wiki/Windows_Driver_Frameworks" title="Windows Driver Frameworks">WDF</a> <ul><li><a href="/wiki/Kernel-Mode_Driver_Framework" title="Kernel-Mode Driver Framework">KMDF</a></li> <li><a href="/wiki/User-Mode_Driver_Framework" title="User-Mode Driver Framework">UMDF</a></li></ul></li> <li><a href="/wiki/Windows_Hardware_Lab_Kit" title="Windows Hardware Lab Kit">Windows HLK</a></li> <li><a href="/wiki/Windows_Driver_Model" title="Windows Driver Model">WDM</a></li></ul> </div></td></tr></tbody></table><div></div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Database</th><td class="navbox-list-with-group navbox-list navbox-odd hlist" style="width:100%;padding:0"><div style="padding:0 0.25em"></div><table class="nowraplinks navbox-subgroup" style="border-spacing:0"><tbody><tr><th scope="row" class="navbox-group" style="width:1%;font-weight:normal;"><a href="/wiki/Microsoft_SQL_Server" title="Microsoft SQL Server">SQL Server</a></th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/SQL_Server_Express" title="SQL Server Express">Express</a></li> <li><a href="/wiki/SQL_Server_Compact" title="SQL Server Compact">Compact</a></li> <li><a href="/wiki/SQL_Server_Management_Studio" title="SQL Server Management Studio">Management Studio</a></li> <li><a href="/wiki/MSDE" title="MSDE">MSDE</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%;font-weight:normal;">SQL services</th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Microsoft_Analysis_Services" title="Microsoft Analysis Services">Analysis</a></li> <li><a href="/wiki/SQL_Server_Reporting_Services" title="SQL Server Reporting Services">Reporting</a></li> <li><a href="/wiki/SQL_Server_Integration_Services" title="SQL Server Integration Services">Integration</a></li> <li><a href="/wiki/SQL_Server_Notification_Services" title="SQL Server Notification Services">Notification</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%;font-weight:normal;">Other</th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Visual_FoxPro" title="Visual FoxPro">Visual FoxPro</a></li> <li><a href="/wiki/Microsoft_Access" title="Microsoft Access">Microsoft Access</a></li> <li><a href="/wiki/Access_Database_Engine" title="Access Database Engine">Access Database Engine</a></li> <li><a href="/wiki/Extensible_Storage_Engine" title="Extensible Storage Engine">Extensible Storage Engine</a></li></ul> </div></td></tr></tbody></table><div></div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Source control</th><td class="navbox-list-with-group navbox-list navbox-even hlist" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Microsoft_Visual_SourceSafe" title="Microsoft Visual SourceSafe">Visual SourceSafe</a></li> <li><a href="/wiki/Azure_DevOps_Server#TFVC" title="Azure DevOps Server">Team Foundation Version Control</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Testing and<br />debugging</th><td class="navbox-list-with-group navbox-list navbox-odd hlist" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/CodeView" title="CodeView">CodeView</a></li> <li><a href="/wiki/OneFuzz" title="OneFuzz">OneFuzz</a></li> <li><a href="/wiki/Playwright_(software)" title="Playwright (software)">Playwright</a></li> <li><a href="/wiki/Microsoft_Script_Debugger" title="Microsoft Script Debugger">Script Debugger</a></li> <li><a href="/wiki/WinDbg" title="WinDbg">WinDbg</a></li> <li><a href="/wiki/XUnit.net" title="XUnit.net">xUnit.net</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Delivery</th><td class="navbox-list-with-group navbox-list navbox-even hlist" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Active_Setup" title="Active Setup">Active Setup</a></li> <li><a href="/wiki/ClickOnce" title="ClickOnce">ClickOnce</a></li> <li><a href="/wiki/Npm_(software)" class="mw-redirect" title="Npm (software)">npm</a></li> <li><a href="/wiki/NuGet" title="NuGet">NuGet</a></li> <li><a href="/wiki/Vcpkg" title="Vcpkg">vcpkg</a></li> <li><a href="/wiki/Web_Platform_Installer" title="Web Platform Installer">Web Platform Installer</a></li> <li><a href="/wiki/Windows_Installer" title="Windows Installer">Windows Installer</a> <ul><li><a href="/wiki/WiX" title="WiX">WiX</a></li></ul></li> <li><a href="/wiki/Windows_Package_Manager" title="Windows Package Manager">Windows Package Manager</a></li> <li><a href="/wiki/Microsoft_Store" title="Microsoft Store">Microsoft Store</a></li></ul> </div></td></tr><tr><td class="navbox-abovebelow" colspan="2"><div><span class="noviewer" typeof="mw:File"><span title="Category"><img alt="" src="//upload.wikimedia.org/wikipedia/en/thumb/9/96/Symbol_category_class.svg/16px-Symbol_category_class.svg.png" decoding="async" width="16" height="16" class="mw-file-element" srcset="//upload.wikimedia.org/wikipedia/en/thumb/9/96/Symbol_category_class.svg/23px-Symbol_category_class.svg.png 1.5x, //upload.wikimedia.org/wikipedia/en/thumb/9/96/Symbol_category_class.svg/31px-Symbol_category_class.svg.png 2x" data-file-width="180" data-file-height="185" /></span></span> <a href="/wiki/Category:Microsoft_development_tools" title="Category:Microsoft development tools">Category</a></div></td></tr></tbody></table></div> <div class="navbox-styles"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1129693374" /><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1236075235" /></div><div role="navigation" class="navbox" aria-labelledby="Microsoft_Research_(MSR)216" style="padding:3px"><table class="nowraplinks mw-collapsible autocollapse navbox-inner" style="border-spacing:0;background:transparent;color:inherit"><tbody><tr><th scope="col" class="navbox-title" colspan="2"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1129693374" /><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1239400231" /><div class="navbar plainlinks hlist navbar-mini"><ul><li class="nv-view"><a href="/wiki/Template:Microsoft_Research" title="Template:Microsoft Research"><abbr title="View this template">v</abbr></a></li><li class="nv-talk"><a href="/wiki/Template_talk:Microsoft_Research" title="Template talk:Microsoft Research"><abbr title="Discuss this template">t</abbr></a></li><li class="nv-edit"><a href="/wiki/Special:EditPage/Template:Microsoft_Research" title="Special:EditPage/Template:Microsoft Research"><abbr title="Edit this template">e</abbr></a></li></ul></div><div id="Microsoft_Research_(MSR)216" style="font-size:114%;margin:0 4em"><a href="/wiki/Microsoft_Research" title="Microsoft Research">Microsoft Research (MSR)</a></div></th></tr><tr><th scope="row" class="navbox-group" style="width:1%">Main<br />projects</th><td class="navbox-list-with-group navbox-list navbox-odd hlist" style="width:100%;padding:0"><div style="padding:0 0.25em"></div><table class="nowraplinks navbox-subgroup" style="border-spacing:0"><tbody><tr><th scope="row" class="navbox-group" style="width:1%">Languages, compilers</th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Bartok_(compiler)" title="Bartok (compiler)">Bartok</a></li> <li><a href="/wiki/Bosque_(programming_language)" title="Bosque (programming language)">Bosque</a></li> <li><a href="/wiki/C%CF%89" class="mw-redirect" title="Cω">Cω</a></li> <li><a href="/wiki/F*_(programming_language)" title="F* (programming language)">F*</a></li> <li><a href="/wiki/Lean_(proof_assistant)" title="Lean (proof assistant)">Lean</a></li> <li><a href="/wiki/P_(programming_language)" title="P (programming language)">P</a></li> <li><a href="/wiki/Project_Verona" title="Project Verona">Project Verona</a></li> <li><a href="/wiki/Microsoft_Phoenix" title="Microsoft Phoenix">Phoenix</a></li> <li><a href="/wiki/Polyphonic_C_Sharp" class="mw-redirect" title="Polyphonic C Sharp">Polyphonic C#</a></li> <li><a href="/wiki/SecPAL" title="SecPAL">SecPAL</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="/wiki/Distributed_computing" title="Distributed computing">Distributed</a>–<a href="/wiki/Grid_computing" title="Grid computing">grid computing</a></th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/BitVault" title="BitVault">BitVault</a></li> <li><a href="/wiki/Confidential_Consortium_Framework" title="Confidential Consortium Framework">Confidential Consortium Framework</a></li> <li><a href="/wiki/DeepSpeed" title="DeepSpeed">DeepSpeed</a></li> <li><a href="/wiki/Orleans_(software_framework)" title="Orleans (software framework)">Orleans</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="/wiki/Internet" title="Internet">Internet</a>, <a href="/wiki/Computer_network" title="Computer network">networking</a></th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li>AjaxView</li> <li><a href="/wiki/Avalanche_(P2P)" title="Avalanche (P2P)">Avalanche</a></li> <li><a href="/wiki/Conference_XP" title="Conference XP">Conference XP</a></li> <li><a href="/wiki/Gazelle_(web_browser)" title="Gazelle (web browser)">Gazelle</a></li> <li><a href="/wiki/HoneyMonkey" title="HoneyMonkey">HoneyMonkey</a></li> <li><a href="/wiki/Penny_Black_(research_project)" title="Penny Black (research project)">Penny Black</a></li> <li><a href="/wiki/Wallop" title="Wallop">Wallop</a></li> <li><a href="/wiki/WikiBhasha" title="WikiBhasha">WikiBhasha</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Other projects</th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Microsoft_Automatic_Graph_Layout" title="Microsoft Automatic Graph Layout">Automatic Graph Layout</a></li> <li><a href="/wiki/Microsoft_Cognitive_Toolkit" title="Microsoft Cognitive Toolkit">Cognitive Toolkit</a></li> <li><a href="/wiki/Project_Digits" title="Project Digits">Digits</a></li> <li><a href="/wiki/Microsoft_Holoportation" title="Microsoft Holoportation">Holoportation</a></li> <li><a href="/wiki/IllumiRoom" title="IllumiRoom">IllumiRoom</a></li> <li><a href="/wiki/Image_Composite_Editor" title="Image Composite Editor">Image Composite Editor</a></li> <li><a href="/wiki/Infer.NET" title="Infer.NET">Infer.NET</a></li> <li><a href="/wiki/LightGBM" title="LightGBM">LightGBM</a></li> <li><a href="/wiki/LiveStation" title="LiveStation">LiveStation</a></li> <li><a href="/wiki/MyLifeBits" title="MyLifeBits">MyLifeBits</a></li> <li><a href="/wiki/Neural_Network_Intelligence" title="Neural Network Intelligence">Neural Network Intelligence</a></li> <li><a href="/wiki/NodeXL" title="NodeXL">NodeXL</a></li> <li><a href="/wiki/OneFuzz" title="OneFuzz">OneFuzz</a></li> <li><a href="/wiki/PhotoDNA" title="PhotoDNA">PhotoDNA</a></li> <li><a href="/wiki/Microsoft_SEAL" title="Microsoft SEAL">SEAL</a></li> <li><a href="/wiki/SLAM_project" title="SLAM project">SLAM</a></li> <li><a href="/wiki/T2_Temporal_Prover" title="T2 Temporal Prover">T2 Temporal Prover</a></li> <li><a href="/wiki/WorldWide_Telescope" title="WorldWide Telescope">WorldWide Telescope</a></li> <li><a href="/wiki/Z3_Theorem_Prover" title="Z3 Theorem Prover">Z3 Theorem Prover</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="/wiki/Operating_system" title="Operating system">Operating systems</a></th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Barrelfish_(operating_system)" title="Barrelfish (operating system)">Barrelfish</a></li> <li><a href="/wiki/HomeOS" title="HomeOS">HomeOS</a></li> <li><a href="/wiki/Midori_(operating_system)" title="Midori (operating system)">Midori</a></li> <li><a href="/wiki/Singularity_(operating_system)" title="Singularity (operating system)">Singularity</a></li> <li><a href="/wiki/Verve_(operating_system)" title="Verve (operating system)">Verve</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="/wiki/API" title="API">APIs</a></th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Accelerator_(library)" title="Accelerator (library)">Accelerator</a></li> <li><a href="/wiki/Dryad_(programming)" title="Dryad (programming)">Dryad</a></li> <li><a href="/wiki/Joins_(concurrency_library)" title="Joins (concurrency library)">Joins</a></li> <li><a href="/wiki/Mimalloc" title="Mimalloc">mimalloc</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Launched as products</th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/C_Sharp_(programming_language)" title="C Sharp (programming language)">C#</a></li> <li><a href="/wiki/Microsoft_Comic_Chat" title="Microsoft Comic Chat">Comic Chat</a></li> <li><a href="/wiki/Microsoft_Detours" title="Microsoft Detours">Detours</a></li> <li><a href="/wiki/F_Sharp_(programming_language)" title="F Sharp (programming language)">F#</a></li> <li><a href="/wiki/Windows_Desktop_Gadgets" title="Windows Desktop Gadgets">Sideshow</a></li> <li><a href="/wiki/Microsoft_PixelSense" title="Microsoft PixelSense">PixelSense</a> (<a href="/wiki/TouchLight" title="TouchLight">TouchLight</a>)</li> <li><a href="/wiki/Microsoft_SenseCam" title="Microsoft SenseCam">SenseCam</a></li> <li><a href="/wiki/ClearType" title="ClearType">ClearType</a></li> <li><a href="/wiki/Group_Shot" title="Group Shot">Group Shot</a></li> <li><a href="/wiki/Allegiance_(video_game)" title="Allegiance (video game)">Allegiance</a></li> <li><a href="/wiki/TrueSkill" title="TrueSkill">TrueSkill</a></li> <li><a href="/wiki/Microsoft_Songsmith" class="mw-redirect" title="Microsoft Songsmith">Songsmith</a></li> <li><a href="/wiki/Xbox" title="Xbox">Xbox</a> <ul><li><a href="/wiki/Kinect" title="Kinect">Kinect</a></li></ul></li></ul> </div></td></tr></tbody></table><div></div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">MSR Labs<br />applied<br />research</th><td class="navbox-list-with-group navbox-list navbox-odd hlist" style="width:100%;padding:0"><div style="padding:0 0.25em"></div><table class="nowraplinks navbox-subgroup" style="border-spacing:0"><tbody><tr><th scope="row" class="navbox-group" style="width:1%"><a href="/wiki/Microsoft_Live_Labs" title="Microsoft Live Labs">Live Labs</a></th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em"></div><table class="nowraplinks navbox-subgroup" style="border-spacing:0"><tbody><tr><th scope="row" class="navbox-group" style="width:1%">Current</th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Microsoft_Live_Labs_Pivot" title="Microsoft Live Labs Pivot">Pivot</a></li> <li><a href="/wiki/Seadragon_Software" title="Seadragon Software">Seadragon</a> <ul><li><a href="/wiki/Deep_Zoom" title="Deep Zoom">Deep Zoom</a></li></ul></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Discontinued</th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Microsoft_Live_Labs_Deepfish" title="Microsoft Live Labs Deepfish">Deepfish</a></li> <li><a href="/wiki/Microsoft_Live_Labs_Listas" title="Microsoft Live Labs Listas">Listas</a></li> <li><a href="/wiki/Live_Clipboard" title="Live Clipboard">Live Clipboard</a></li> <li><a href="/wiki/Photosynth" title="Photosynth">Photosynth</a></li></ul> </div></td></tr></tbody></table><div></div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="/wiki/Microsoft_FUSE_Labs" title="Microsoft FUSE Labs">FUSE Labs</a></th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Docs.com" title="Docs.com">Docs.com</a></li> <li><a href="/wiki/Kodu_Game_Lab" title="Kodu Game Lab">Kodu</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Other labs</th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Microsoft_Academic_Search" title="Microsoft Academic Search">Academic Search</a></li> <li><a href="/wiki/Microsoft_adCenter_Labs" title="Microsoft adCenter Labs">adCenter Labs</a></li> <li><a href="/wiki/Microsoft_Office" title="Microsoft Office">Office Labs</a></li></ul> </div></td></tr></tbody></table><div></div></td></tr><tr><td class="navbox-abovebelow" colspan="2"><div><span class="noviewer" typeof="mw:File"><span title="Category"><img alt="" src="//upload.wikimedia.org/wikipedia/en/thumb/9/96/Symbol_category_class.svg/16px-Symbol_category_class.svg.png" decoding="async" width="16" height="16" class="mw-file-element" srcset="//upload.wikimedia.org/wikipedia/en/thumb/9/96/Symbol_category_class.svg/23px-Symbol_category_class.svg.png 1.5x, //upload.wikimedia.org/wikipedia/en/thumb/9/96/Symbol_category_class.svg/31px-Symbol_category_class.svg.png 2x" data-file-width="180" data-file-height="185" /></span></span> <a href="/wiki/Category:Microsoft_Research" title="Category:Microsoft Research">Category</a></div></td></tr></tbody></table></div>    </div><noscript><img src="https://auth.wikimedia.org/loginwiki/wiki/Special:CentralAutoLogin/start?useformat=desktop&type=1x1&usesul3=1" alt="" width="1" height="1" style="border: none; position: absolute;"></noscript> <div class="printfooter" data-nosnippet="">Retrieved from "<a dir="ltr" href="https://en.wikipedia.org/w/index.php?title=Dafny&oldid=1265861302">https://en.wikipedia.org/w/index.php?title=Dafny&oldid=1265861302</a>"</div></div> <div id="catlinks" class="catlinks" data-mw="interface"><div id="mw-normal-catlinks" class="mw-normal-catlinks"><a href="/wiki/Help:Category" title="Help:Category">Categories</a>: <ul><li><a href="/wiki/Category:Academic_programming_languages" title="Category:Academic programming languages">Academic programming languages</a></li><li><a href="/wiki/Category:Experimental_programming_languages" title="Category:Experimental programming languages">Experimental programming languages</a></li><li><a href="/wiki/Category:Microsoft_free_software" title="Category:Microsoft free software">Microsoft free software</a></li><li><a href="/wiki/Category:Microsoft_programming_languages" title="Category:Microsoft programming languages">Microsoft programming languages</a></li><li><a href="/wiki/Category:Microsoft_Research" title="Category:Microsoft Research">Microsoft Research</a></li><li><a href="/wiki/Category:Programming_languages_created_in_2009" title="Category:Programming languages created in 2009">Programming languages created in 2009</a></li><li><a href="/wiki/Category:Proof_assistants" title="Category:Proof assistants">Proof assistants</a></li><li><a href="/wiki/Category:Software_using_the_MIT_license" title="Category:Software using the MIT license">Software using the MIT license</a></li><li><a href="/wiki/Category:Statically_typed_programming_languages" title="Category:Statically typed programming languages">Statically typed programming languages</a></li></ul></div><div id="mw-hidden-catlinks" class="mw-hidden-catlinks mw-hidden-cats-hidden">Hidden categories: <ul><li><a href="/wiki/Category:Articles_with_short_description" title="Category:Articles with short description">Articles with short description</a></li><li><a href="/wiki/Category:Short_description_matches_Wikidata" title="Category:Short description matches Wikidata">Short description matches Wikidata</a></li><li><a href="/wiki/Category:All_articles_with_unsourced_statements" title="Category:All articles with unsourced statements">All articles with unsourced statements</a></li><li><a href="/wiki/Category:Articles_with_unsourced_statements_from_January_2023" title="Category:Articles with unsourced statements from January 2023">Articles with unsourced statements from January 2023</a></li><li><a href="/wiki/Category:Articles_needing_additional_references_from_January_2018" title="Category:Articles needing additional references from January 2018">Articles needing additional references from January 2018</a></li><li><a href="/wiki/Category:All_articles_needing_additional_references" title="Category:All articles needing additional references">All articles needing additional references</a></li></ul></div></div> </div> </main> </div> <div class="mw-footer-container"> <footer id="footer" class="mw-footer" > <ul id="footer-info"> <li id="footer-info-lastmod"> This page was last edited on 29 December 2024, at 01:09<span class="anonymous-show"> (UTC)</span>.</li> <li id="footer-info-copyright">Text is available under the <a href="/wiki/Wikipedia:Text_of_the_Creative_Commons_Attribution-ShareAlike_4.0_International_License" title="Wikipedia:Text of the Creative Commons Attribution-ShareAlike 4.0 International License">Creative Commons Attribution-ShareAlike 4.0 License</a>; additional terms may apply. By using this site, you agree to the <a href="https://foundation.wikimedia.org/wiki/Special:MyLanguage/Policy:Terms_of_Use" class="extiw" title="foundation:Special:MyLanguage/Policy:Terms of Use">Terms of Use</a> and <a href="https://foundation.wikimedia.org/wiki/Special:MyLanguage/Policy:Privacy_policy" class="extiw" title="foundation:Special:MyLanguage/Policy:Privacy policy">Privacy Policy</a>. Wikipedia® is a registered trademark of the <a rel="nofollow" class="external text" href="https://wikimediafoundation.org/">Wikimedia Foundation, Inc.</a>, a non-profit organization.</li> </ul> <ul id="footer-places"> <li id="footer-places-privacy"><a href="https://foundation.wikimedia.org/wiki/Special:MyLanguage/Policy:Privacy_policy">Privacy policy</a></li> <li id="footer-places-about"><a href="/wiki/Wikipedia:About">About Wikipedia</a></li> <li id="footer-places-disclaimers"><a href="/wiki/Wikipedia:General_disclaimer">Disclaimers</a></li> <li id="footer-places-contact"><a href="//en.wikipedia.org/wiki/Wikipedia:Contact_us">Contact Wikipedia</a></li> <li id="footer-places-wm-codeofconduct"><a href="https://foundation.wikimedia.org/wiki/Special:MyLanguage/Policy:Universal_Code_of_Conduct">Code of Conduct</a></li> <li id="footer-places-developers"><a href="https://developer.wikimedia.org">Developers</a></li> <li id="footer-places-statslink"><a href="https://stats.wikimedia.org/#/en.wikipedia.org">Statistics</a></li> <li id="footer-places-cookiestatement"><a href="https://foundation.wikimedia.org/wiki/Special:MyLanguage/Policy:Cookie_statement">Cookie statement</a></li> <li id="footer-places-mobileview"><a href="//en.m.wikipedia.org/w/index.php?title=Dafny&mobileaction=toggle_view_mobile" class="noprint stopMobileRedirectToggle">Mobile view</a></li> </ul> <ul id="footer-icons" class="noprint"> <li id="footer-copyrightico"><a href="https://www.wikimedia.org/" class="cdx-button cdx-button--fake-button cdx-button--size-large cdx-button--fake-button--enabled"><picture><source media="(min-width: 500px)" srcset="/static/images/footer/wikimedia-button.svg" width="84" height="29"><img src="/static/images/footer/wikimedia.svg" width="25" height="25" alt="Wikimedia Foundation" lang="en" loading="lazy"></picture></a></li> <li id="footer-poweredbyico"><a href="https://www.mediawiki.org/" class="cdx-button cdx-button--fake-button cdx-button--size-large cdx-button--fake-button--enabled"><picture><source media="(min-width: 500px)" srcset="/w/resources/assets/poweredby_mediawiki.svg" width="88" height="31"><img src="/w/resources/assets/mediawiki_compact.svg" alt="Powered by MediaWiki" lang="en" width="25" height="25" loading="lazy"></picture></a></li> </ul> </footer> </div> </div> </div> <div class="vector-header-container vector-sticky-header-container"> <div id="vector-sticky-header" class="vector-sticky-header"> <div class="vector-sticky-header-start"> <div class="vector-sticky-header-icon-start vector-button-flush-left vector-button-flush-right" aria-hidden="true"> <button class="cdx-button cdx-button--weight-quiet cdx-button--icon-only vector-sticky-header-search-toggle" tabindex="-1" data-event-name="ui.vector-sticky-search-form.icon"><span class="vector-icon mw-ui-icon-search mw-ui-icon-wikimedia-search"></span> <span>Search</span> </button> </div> <div role="search" class="vector-search-box-vue vector-search-box-show-thumbnail vector-search-box"> <div class="vector-typeahead-search-container"> <div class="cdx-typeahead-search cdx-typeahead-search--show-thumbnail"> <form action="/w/index.php" id="vector-sticky-search-form" class="cdx-search-input cdx-search-input--has-end-button"> <div class="cdx-search-input__input-wrapper" data-search-loc="header-moved"> <div class="cdx-text-input cdx-text-input--has-start-icon"> <input class="cdx-text-input__input" type="search" name="search" placeholder="Search Wikipedia"> <span class="cdx-text-input__icon cdx-text-input__start-icon"></span> </div> <input type="hidden" name="title" value="Special:Search"> </div> <button class="cdx-button cdx-search-input__end-button">Search</button> </form> </div> </div> </div> <div class="vector-sticky-header-context-bar"> <nav aria-label="Contents" class="vector-toc-landmark"> <div id="vector-sticky-header-toc" class="vector-dropdown mw-portlet mw-portlet-sticky-header-toc vector-sticky-header-toc vector-button-flush-left" > <input type="checkbox" id="vector-sticky-header-toc-checkbox" role="button" aria-haspopup="true" data-event-name="ui.dropdown-vector-sticky-header-toc" class="vector-dropdown-checkbox " aria-label="Toggle the table of contents" > <label id="vector-sticky-header-toc-label" for="vector-sticky-header-toc-checkbox" class="vector-dropdown-label cdx-button cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--weight-quiet cdx-button--icon-only " aria-hidden="true" ><span class="vector-icon mw-ui-icon-listBullet mw-ui-icon-wikimedia-listBullet"></span> <span class="vector-dropdown-label-text">Toggle the table of contents</span> </label> <div class="vector-dropdown-content"> <div id="vector-sticky-header-toc-unpinned-container" class="vector-unpinned-container"> </div> </div> </div> </nav> <div class="vector-sticky-header-context-bar-primary" aria-hidden="true" ><span class="mw-page-title-main">Dafny</span></div> </div> </div> <div class="vector-sticky-header-end" aria-hidden="true"> <div class="vector-sticky-header-icons"> <a href="#" class="cdx-button cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--weight-quiet cdx-button--icon-only" id="ca-talk-sticky-header" tabindex="-1" data-event-name="talk-sticky-header"><span class="vector-icon mw-ui-icon-speechBubbles mw-ui-icon-wikimedia-speechBubbles"></span> <span></span> </a> <a href="#" class="cdx-button cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--weight-quiet cdx-button--icon-only" id="ca-subject-sticky-header" tabindex="-1" data-event-name="subject-sticky-header"><span class="vector-icon mw-ui-icon-article mw-ui-icon-wikimedia-article"></span> <span></span> </a> <a href="#" class="cdx-button cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--weight-quiet cdx-button--icon-only" id="ca-history-sticky-header" tabindex="-1" data-event-name="history-sticky-header"><span class="vector-icon mw-ui-icon-wikimedia-history mw-ui-icon-wikimedia-wikimedia-history"></span> <span></span> </a> <a href="#" class="cdx-button cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--weight-quiet cdx-button--icon-only mw-watchlink" id="ca-watchstar-sticky-header" tabindex="-1" data-event-name="watch-sticky-header"><span class="vector-icon mw-ui-icon-wikimedia-star mw-ui-icon-wikimedia-wikimedia-star"></span> <span></span> </a> <a href="#" class="cdx-button cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--weight-quiet cdx-button--icon-only" id="ca-edit-sticky-header" tabindex="-1" data-event-name="wikitext-edit-sticky-header"><span class="vector-icon mw-ui-icon-wikimedia-wikiText mw-ui-icon-wikimedia-wikimedia-wikiText"></span> <span></span> </a> <a href="#" class="cdx-button cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--weight-quiet cdx-button--icon-only" id="ca-ve-edit-sticky-header" tabindex="-1" data-event-name="ve-edit-sticky-header"><span class="vector-icon mw-ui-icon-wikimedia-edit mw-ui-icon-wikimedia-wikimedia-edit"></span> <span></span> </a> <a href="#" class="cdx-button cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--weight-quiet cdx-button--icon-only" id="ca-viewsource-sticky-header" tabindex="-1" data-event-name="ve-edit-protected-sticky-header"><span class="vector-icon mw-ui-icon-wikimedia-editLock mw-ui-icon-wikimedia-wikimedia-editLock"></span> <span></span> </a> </div> <div class="vector-sticky-header-buttons"> <button class="cdx-button cdx-button--weight-quiet mw-interlanguage-selector" id="p-lang-btn-sticky-header" tabindex="-1" data-event-name="ui.dropdown-p-lang-btn-sticky-header"><span class="vector-icon mw-ui-icon-wikimedia-language mw-ui-icon-wikimedia-wikimedia-language"></span> <span>3 languages</span> </button> <a href="#" class="cdx-button cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--weight-quiet cdx-button--action-progressive" id="ca-addsection-sticky-header" tabindex="-1" data-event-name="addsection-sticky-header"><span class="vector-icon mw-ui-icon-speechBubbleAdd-progressive mw-ui-icon-wikimedia-speechBubbleAdd-progressive"></span> <span>Add topic</span> </a> </div> <div class="vector-sticky-header-icon-end"> <div class="vector-user-links"> </div> </div> </div> </div> </div> <div class="mw-portlet mw-portlet-dock-bottom emptyPortlet" id="p-dock-bottom"> <ul> </ul> </div> <script>(RLQ=window.RLQ||[]).push(function(){mw.config.set({"wgHostname":"mw-web.codfw.main-7ccc697c5f-6rcrz","wgBackendResponseTime":159,"wgPageParseReport":{"limitreport":{"cputime":"0.493","walltime":"1.054","ppvisitednodes":{"value":2524,"limit":1000000},"postexpandincludesize":{"value":145387,"limit":2097152},"templateargumentsize":{"value":2504,"limit":2097152},"expansiondepth":{"value":27,"limit":100},"expensivefunctioncount":{"value":8,"limit":500},"unstrip-depth":{"value":1,"limit":20},"unstrip-size":{"value":85083,"limit":5000000},"entityaccesscount":{"value":0,"limit":400},"timingprofile":["100.00% 668.787 1 -total"," 19.17% 128.208 1 Template:Reflist"," 18.76% 125.475 10 Template:Navbox"," 15.94% 106.618 2 Template:Infobox"," 14.91% 99.716 6 Template:Cite_conference"," 14.51% 97.034 1 Template:Microsoft_FOSS"," 11.53% 77.085 1 Template:Short_description"," 10.87% 72.680 1 Template:Infobox_programming_language"," 6.67% 44.584 2 Template:Pagetype"," 6.29% 42.077 1 Template:Infobox_software/simple"]},"scribunto":{"limitreport-timeusage":{"value":"0.272","limit":"10.000"},"limitreport-memusage":{"value":6624678,"limit":52428800}},"cachereport":{"origin":"mw-web.codfw.main-65585cc8dc-4m6xf","timestamp":"20250401004818","ttl":2589106,"transientcontent":true}}});});</script> <script type="application/ld+json">{"@context":"https:\/\/schema.org","@type":"Article","name":"Dafny","url":"https:\/\/en.wikipedia.org\/wiki\/Dafny","sameAs":"http:\/\/www.wikidata.org\/entity\/Q48989398","mainEntity":"http:\/\/www.wikidata.org\/entity\/Q48989398","author":{"@type":"Organization","name":"Contributors to Wikimedia projects"},"publisher":{"@type":"Organization","name":"Wikimedia Foundation, Inc.","logo":{"@type":"ImageObject","url":"https:\/\/www.wikimedia.org\/static\/images\/wmf-hor-googpub.png"}},"datePublished":"2017-12-17T20:13:37Z","dateModified":"2024-12-29T01:09:13Z","image":"https:\/\/upload.wikimedia.org\/wikipedia\/commons\/4\/44\/Dafny_logo.jpg","headline":"programming language"}</script> </body> </html>