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

In this case, the precondition is modelled as the preVentricleStartTime function.
We adapt some parts of the Z specification in the Perfect Developer syntax.
For instance, bo mode . chambers sensed

∈{ C DUAL , C VENTRICLE } was

translated to the following Perfect Developer predicate.

c BO MODE . bo mode . chambers sensed = CHAMBERS C VENTRICLE
|

c BO MODE . bo mode . chambers sensed = CHAMBERS C DUAL

Using the precondition, we are able to translate the VentricleStartTime op-
eration from Z to Perfect Developer, including the preVentricleStartTime func-
tion in the pre section, updating the initial time of the ventricular sensed pulse
to the actual time ( c TimeSt ! chg v start time ( c TimeSt . time )) and updating
the value of r wave with the value of the current measurement in ventricle
( c MeasuredParameters ! set r wave ( c TimeSt . v curr measurement )).

schema !VentricularStartTime
pre preVentricularStartTime
post (c_MeasuredParameters!set_r_wave(c_TimeSt.v_curr_measurement)
& c_TimeSt!chg_v_start_time(c_TimeSt.time));

During the translation, we move from logical disjunctions of schemas in Z to
guards in Perfect Developer. Those expressions are equivalent to ' if 'and' else '
statements in languages like C++ or Java . The basic syntax of a guard is
[ precondition ]: expression . It means that for each guard, if the precondition
is satisfied, a predicate expression will be the postcondition of the operation,
else , the next guard will be checked. The operation will check the precondition
of each guard until one is found to be true . If none of the guards are true ,thelast
guard is selected. We include closed brackets '[]' with no preconditions as the
last guard, which means, in Perfect Developer, that if none of the preconditions
are satisfied, the operation will be skipped. Note that there is no global precon-
ditions in the SensingModule operation: the preconditions modelled as boolean
functions like preVentricularMeasurement are included inside the brackets in
each guard in the ' post ' section of the operation.

schema !SensingModule
post ([preVentricularMeasurement]: !VentricularMeasurement,
[preAtrialMeasurement]: !AtrialMeasurement,
[]);

Finally, Z sequential composition is translated into Perfect Developer's then -
constructs. Besides, each schema operation is called using an exclamation mark
' ! ', as illustrated below, where we present the translation of the BradyTherapy
operation, presented in Section 3.

schema !BradyTherapy
post (!SetTimer then !SensingModule
then !SensingMarkers then !SetMode);

end;