# 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] ?