Specification and Verification Tools Seminar
			      Homework 6
		     $Date: 2008/12/02 02:27:34 $

For 3 December 2008. 

Download and install Spark/Ada from
http://www.praxis-his.com/sparkada/sparkbook.asp.

See also http://www.praxis-his.com/sparkada/downloads.asp for more
information. 

PROBLEM

Write the specification of a procedure Solve to solve the following
pair of simultaneous linear equations:

ax + by = p
cx + dy = q

Assume that the coefficients a, b, c and d are integers.  Your task is
to provide full annotations including an appropriate precondition and
postcondition for the following code.

package body M is

   procedure Solve(A, B, C, D : in     Integer;
                   P, Q       : in     Float;
                   X, Y       :    out Float)
   is 
      R : Integer;
   begin
      R := A*D-C*B;
      X:=(Float (D)*P-Float (A)*Q)/Float (R);
      Y:=(Float (A)*Q-Float (C)*P)/Float (R);
   end Solve;
end M;