Packages and Abstract Data Types

• Modeling of Ada type system:
  • Records with function components model Ada packages.
  • Existential quantification models Ada type abstraction.

type Point = Real x Real
type Point1 =
   {makepoint: (Real x Real) $->$ Point,
      x_coord: Point x Real,
      y_coord: Point x Real}

value point1: Point1 =
   {makepoint = fun(x:Real, y:Real)(x, y),
      x_coord = fun(p:Point) fst(p),
      y_coord = fun(p:Point) snd(p)}