From complete unit tests to implementation
The goal of this lecture note is to illustrate how to calculate
implementations from complete specifications. The calculations are
spelled out for Boolean functions (negation, conjunction, negated
conjunction). The resulting definitions only use conditional
expressions.
Mimer: Observational equivalence at work.
Loki: Right. Not iffy at all.
The observational equivalences
- false = false and true are observationally equivalent
- for any expression e,
e = true and e are observationally equivalent
- for any expressions e1 and e2,
if true then e1 else e2 and e1 are observationally equivalent
- for any expressions e1 and e2,
if false then e1 else e2 and e2 are observationally equivalent
- for any expression e,
if e then true then false and e are observationally equivalent
- for any pure expression v,
if v then false else false and false are observationally equivalent
- for any expressions e1, e2, and e3,
not (if e1 then e2 else e3) and if e1 then not e2 else not e3 are observationally equivalent
Negation
...see the resource file...
Conjunction
...see the resource file...
Negated conjunction (nand)
...see the resource file...
Version
Created
[16 Mar 2020]