Go backward to A Figures Package Go up to Top Go forward to Record Types and Inheritance

Bounded Quantification

• Type inclusion:
  • Type A is included in (a subtype of) type B when all values of A are also values of B.
  • Inclusion relation on subranges, records, variants, function, universally and existentially quantified types.
• Integer subrange type n ...m
  • n ...m <= n' <=m' iff n' <= n and m <= m'
  • value f = fun(x: 2..5) x+1
    f: 2..5 -> 3..6
    f(3)
    value g = fun(y: 3..4) f(y)
• Function type
  • s -> t <= s' -> t' iff s' <= s and t <= t'
  • Function of type 3 ...7 can be also considered as function of type 4 ...6 ->6 ...10