Function refinement
f' : Nat -> Nat \not<= f : Int -> Int
Functions
-- as a service
contravariance
domain
-- restrictions for the client
range
-- obligations for server
slide
:
The function subtype relation
