{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T11:21:30Z","timestamp":1725448890636},"reference-count":0,"publisher":"EasyChair","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>A recursive function is well defined if its every recursive call<\/jats:p><jats:p>corresponds a decrease in some well-founded order.  Such a function is<\/jats:p><jats:p>said to be _terminating_ and is in many applications the standard way<\/jats:p><jats:p>to define a function.  A boolean function can also be defined as<\/jats:p><jats:p>an extreme solution to a recurrence relation, that is, as a least or<\/jats:p><jats:p>greatest fixpoint of some functor.  Such _extreme predicates_ are<\/jats:p><jats:p>useful to encode a set of inductive or coinductive inference rules<\/jats:p><jats:p>and are at the core of many a constructive logic.  The<\/jats:p><jats:p>verification-aware programming language Dafny supports both<\/jats:p><jats:p>terminating functions and extreme predicates.  This tutorial<\/jats:p><jats:p>describes the difference in general terms, and then describes novel<\/jats:p><jats:p>syntactic support in Dafny for defining and proving lemmas with<\/jats:p><jats:p>extreme predicates.  Various examples and considerations are given.<\/jats:p><jats:p>Although Dafny's verifier has at its core a first-order SMT solver,<\/jats:p><jats:p>Dafny's logical encoding makes it possible to reason about fixpoints<\/jats:p><jats:p>in an automated way.<\/jats:p>","DOI":"10.29007\/v2m3","type":"proceedings-article","created":{"date-parts":[[2018,1,23]],"date-time":"2018-01-23T18:04:19Z","timestamp":1516730659000},"page":"52-36","source":"Crossref","is-referenced-by-count":1,"title":["Well-founded Functions and Extreme Predicates in Dafny: A Tutorial"],"prefix":"10.29007","volume":"40","author":[{"given":"Rustan","family":"Leino","sequence":"first","affiliation":[]}],"member":"11545","event":{"name":"IWIL-2015. 11th International Workshop on the Implementation of Logics"},"container-title":["EPiC Series in Computing"],"original-title":[],"deposited":{"date-parts":[[2018,1,23]],"date-time":"2018-01-23T18:04:21Z","timestamp":1516730661000},"score":1,"resource":{"primary":{"URL":"https:\/\/easychair.org\/publications\/paper\/vHsB"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"references-count":0,"URL":"https:\/\/doi.org\/10.29007\/v2m3","relation":{},"ISSN":["2398-7340"],"issn-type":[{"type":"print","value":"2398-7340"}],"subject":[]}}