Specifications of imperative programs Acceptable Acceptable Initial State Final State “Xis “Y is the greater than square root Zero” Action ofX” of the Program 6/197 Specifications of imperative programs 6 / 197