Content deleted Content added
→Assignment: Correct the use of substitution notation from normal brackets to square brackets. |
Citation bot (talk | contribs) Add: s2cid. | Use this bot. Report bugs. | Suggested by Abductive | #UCB_webform 1483/3850 |
||
Line 272:
In predicate transformers semantics, expressions are restricted to terms of the logic (see above). However, this restriction seems too strong for most existing programming languages, where expressions may have side effects (call to a function having a side effect), may not terminate or abort (like ''division by zero''). There are many proposals to extend weakest-preconditions or strongest-postconditions for imperative expression languages and in particular for [[Monad (functional programming)|monads]].
Among them, ''Hoare Type Theory'' combines [[Hoare logic]] for a [[Haskell (programming language)|Haskell]]-like language, [[separation logic]] and [[type theory]].<ref>{{cite journal |first1=Aleksandar |last1=Nanevski |first2=Greg |last2=Morrisett |first3=Lars |last3=Birkedal |title=Hoare Type Theory, Polymorphism and Separation |journal=Journal of Functional Programming |volume=18 |issue=5–6 |pages=865–911 |date=September 2008 |doi=10.1017/S0956796808006953 |s2cid=6956622 |url=http://ynot.cs.harvard.edu/papers/jfpsep07.pdf }}</ref>
This system is currently implemented as a [[Coq]] library called '''Ynot'''.<ref>[http://ynot.cs.harvard.edu/ Ynot] a [[Coq]] library implementing Hoare Type Theory.</ref> In this language, [[Evaluation strategy|evaluation of expressions]] corresponds to computations of ''strongest-postconditions''.
| |||