This overview considers the most general case: relations. Programs map elements of a Domain into elements from a Range.
P is a piece of text, a "program" [P] "box P" is a relation, the "meaning of P", or its semanticsIf we have some Domain (let's say, Integer I), and some Range (let's also say Integer I), then box P is a mapping
[P] : I --> IThis should look quite familiar from our studies in ML.
Verification has 2 major approaches: testing and proof.
Functional semantics give us a succinct way to express the properties that need to be demonstrated, either via testing or proof.
correctness is this: dom(r intersect [P]) = dom(r)Examples:
r: { (1,21), (2,102), (2, 107), (8,-5), (9,21), (9,31) } [P1]: { (1,43), (1,21), (2,102), (9,21) } [P2]: { (1,43), (2,107), (8,-5), (9,21) } [P3]: { (1,21), (2,107), (8,-5), (9,31), (43,1101) } correct
correctness is this: f subset [P]Examples:
f: { (1,21), (2,102), (8,-5), (9,21) } [P1]: { (1,43), (1,21), (2,102), (9,21) } [P1a]: { (1,43), (1,21), (2,102), (9,21), (8, -5) } [P2]: { (1,21), (2,102), (9,21) } [P3]: { (1,21), (2,102), (8,-5), (9,21) } correct [P4]: { (1,21), (2,102), (8,-5), (9,31), (43,117) } correct