Including the limit of parameters, the restrictions of the return value, and the limit of the class status, there is an automatic UnitTest! ! ! ! ! Long Square_root (long x) IN // Parameter {Assert (x> = 0);} OUT (RESULT) // Return {Assert ((Result * Result) == x);} body {return math.sqrt (x) Class Date {Int day; int hour; invariant // class status {Assert (1 <= day && day <= 31); assert (0 <= Hour && Hour <24);}}} D to UnitTest's support Class Sum {int Add (int x, int y) {return x y;} UnitTest {Assert (add (3,4) == 7); assert (add (-2, 0) == -2);}} UnitTest will be called automatically before Main
