/* * Lab 4 - Exercise 3. * * Specification of array maximum. */ MACHINE ArrayMax (nn) CONSTRAINTS nn : NAT1 OPERATIONS res <-- maximum (aa) = PRE aa : 1..nn --> INT THEN res := max(ran(aa)) END END