package Relational --# own X; --# initializes X; is X : Integer := 0; -- Figure 3 procedure Inc; --# global in out X; --# derives X from X; --# post X = X~ + 1; end Relational; package body Relational is -- Figure 3 procedure Inc is begin X := X + 1; end Inc; end Relational;