Formal Development of a Cardiac Pacemaker: From Specification to Code - Formal Methods: Foundations and Applications - page 217

class TimeSt ^=
abstract
var time : int;
var a_start_time, a_max, a_delay : int;
var v_start_time, v_max, v_delay : int;
var a_curr_measurement, v_curr_measurement : int;
interface
function time, a_start_time, a_max, a_delay;
function v_start_time, v_max, v_delay;
function a_curr_measurement, v_curr_measurement;
build{!time : int,
!a_start_time : int, !a_max : int, !a_delay : int,
!v_start_time : int, !v_max : int, !v_delay : int,
!a_curr_measurement : int, !v_curr_measurement : int};
schema !chg_time(x:int)
post time! = x;
...
end;
The variables declared in the abstract section that are available to derived
classes, must be included as functions in the interface section of the class. This
is the case for all variables in the class TimeSt . We do not restrict any initial value
for TimeSt variables, we only need to initiate the variables in the build function.
This concludes the translation of the TimeSt component of the PulseGenerator
into a Perfect Developer class.
A schema operation starts with the schema keyword, followed by the name
of the schema prefixed by an exclamation mark ' ! '. When the operation has
preconditions, they are included after the keyword pre . Finally, the postcondition
of the operation is included after the keyword post , with each variable that is
changed followed by an exclamation mark. For example, we have the chg time
schema presented above, in which only the variable time is updated.
Regarding the system composition, one of our main requirements whilst mov-
ing into Perfect Developer was to keep the modularisation of the system as in
the Z specification. We were able to find a way to keep this modularisation in
the translation of the PulseGenerator into Perfect Developer, by creating a new
class PulseGenerator and instances of each component like TimeSt in the ab-
stract section. In order to help us to identify which variables in PulseGenerator
are declared as an instance of a component, we declare the variable as the name
of the corresponding class, but prefixed by c . For example, we declare an in-
stance of TimeSt as var c TimeSt : TimeSt in the main class PulseGenerator .
final class PulseGenerator ^=
abstract
var c_TimeSt : TimeSt;
var c_ProgrammableParameters : ProgrammableParameters;
var c_SensingPulse : SensingPulse;
var c_PacingPulse : PacingPulse;
var c_MeasuredParameters : MeasuredParameters;
...