procedure UniversalAnswer(var a : Integer);
require
   a = 42;
begin
   // code here
ensure
   a = 42;
end;