Functional Semantics

OVERVIEW

Programs are text. We would like to think of programs as having some meaning, that is, producing something. Normally we think of programs as computing functions.

This overview considers the most general case: relations. Programs map elements of a Domain into elements from a Range.

Notation

P    is a piece of text, a "program"

[P]  "box P" is a relation, the "meaning of P", or its semantics
If 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 --> I
This should look quite familiar from our studies in ML.

Programs vs. Specs

Developing software (SE) requires that we specify the computation we want, and write a program that we think gives us what we want. One major problem in SE is deciding, or showing, that indeed our program conforms to the spec. We call this verification. (Recall that validation is showing that the program meets the requirements).

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.

Consider a spec r, which is a relation (function is a special case). 
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
Consider a spec f, which is a function (special case of a relation). 
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

The Question (one of them)...

How can we decide, given P, what is [P] ?

This is denotational semantics of programs and languages.