C.6. Contracts - JulTob/Ada GitHub Wiki

You can reinforce behaviours in the program by contract conditioning.

Strong typing is already a form of contract reinforcement.

Contract programming states that

The use of processes establishes a contract between the computer and the users. If certain parameters are met, then it will perform an action or return some data. Reinforcing these contracts is the role of a programmer.

The validation of these conditions is the core of contract programming.

The conditions that should be met by the client (the user) are called preconditions, and the conditions that are to be met by the provider (the program) are called postconditions.

function Division( Up, Down: Float) return Float
   with 
      Pre =>  -- Non zero division forbiden
         Down /= 0.0,
      Post => -- Result about equal to inverse operation?
         Division'Result * Down < Up + 0.00001 
         and then
         Division'Result * Down > Up - 0.00001;
         -- Floats do not have a good behaviour with = (comparing equal to)
         -- so it checks in a boundary.
    ...

procedure Inc(V: in out Integer)
   with 
      Pre => 
         V < Integer'Last,
      Post =>
         V = V'OLD +1;

V'Old is the value V had before entering the procedure.