Binary Relations

Consider a simpler problem of determining when one binary relation satisfies another. Suppose we have a specification for a square_root procedure:

1

 squareĒ_root(x: int)/ok(int)

		pre   

		post    

that denotes the binary relation:

I could choose to implement this procedure such that I always return the positive square root of an integer. Its relation is:

Informally, my implementation satisfies the specification because just narrows the possible choice of the integer returned allowed by and the implementation defines some value for each input integer that is defined for the specification.

More formally, we have, given an abstract relation, , and a concrete relation, :

The first property says that any pair in the concrete relation is also an element of the abstract relation. The second property says that for each input that is related by , we want to be defined. Without the second property, could be empty and the satisfies relation would hold.