/* * Lab 4 - Exercise 2. * * Specification of square root. */ MACHINE SquareRoot DEFINITIONS square (xx) == ((xx) * (xx)) OPERATIONS res <-- sqrt (xx) = PRE xx : NAT THEN ANY nn WHERE nn : NAT & square(nn) <= xx & xx < square(nn + 1) THEN res := nn END END END