cid 1093c057eff74a7abeff16ff10db3ffebf206793171abe3d1431c82366529372 · original · open access · via wikipedia
Title: Dafny Authors: Venue: Wikipedia Year: unknown Canonical: wiki:dafny URL: https://en.wikipedia.org/wiki/Dafny Collector: wikipedia OA: true ABSTRACT Dafny is an imperative and functional compiled language that compiles to other programming languages, such as C#, Java, JavaScript, Go, and Python. It supports formal specification through preconditions, postconditions, loop invariants, loop variants, termination specifications and read/write framing specifications. The language combines ideas from the functional programming and imperative programming paradigms; it includes support for object-oriented programming. Features include generic classes, dynamic allocation, inductive datatypes and a variation of separation logic known as implicit dynamic frames for reasoning about side effects. Dafny was created by Rustan Leino at Microsoft Research after his prior work on developing ESC/Modula-3, ESC/Java, and Spec#.