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

Next, we have to declare all the variables of the class, those components
of the state, as function in the interface section. It allows us to have access
to its internal variables and schema operations. Finally, before translating the
operations of the class, we have to declare the build function, which defines the
initial values of the state. The variables declared in the build function will be
translated to the parameters in the constructor of the class in languages like C#.
final class PulseGenerator ^=
...
interface
function c_TimeSt, c_ProgrammableParameters, c_MeasuredParameters;
...
function c_SensingPulse, function c_PacingPulse;
build{!c_TimeSt : TimeSt, !c_MeasuredParameters : MeasuredParameters,
!c_ProgrammableParameters : ProgrammableParameters,
!c_SensingPulse : SensingPulse, !c_PacingPulse : PacingPulse, ...};
...
The translation of the operations of the PulseGenerator to Perfect Devel-
oper is illustrated below, where we present the translation of the SetTimer Z
operation. The syntax of an invocation of a component is a little bit different
from that used to access a variable. In the PulseGenerator class, we access the
variable time , for example, with the predicate c TimeSt . time . However, we call
an operation of the c TimeSt component as c TimeSt ! chg time ( ... ). Finally,
we translate the SetTimer operation to a new schema operation of the class
PulseGenerator that calls the operation chg time and increments the actual
time, c TimeSt . time .
final class PulseGenerator ^=
...
schema !SetTimer
post (c_TimeSt!chg_time(c_TimeSt.time + 1));
...
As discussed above, a schema operation in Z is slightly different from its
equivalent in Perfect Developer. Precondition and postcondition are separated
in pre and post sections in Perfect Developer schemas. We use boolean func-
tions to model the precondition of each schema operation in Perfect Developer.
This approach allows the reuse of the precondition function every time we need
to include the same precondition in an operation. In order to keep a compre-
hensible code, we established that a boolean function as the precondition of an
operation is named with the prefix pre . First, we present the precondition of the
VentricleStartTime operation.
function preVentricularStartTime : bool
^= (c_BO_MODE.bo_mode.chambers_sensed = CHAMBERS C_DUAL
| c_BO_MODE.bo_mode.chambers_sensed = CHAMBERS C_VENTRICLE)
& ((c_TimeSt.v_curr_measurement
> c_MeasuredParameters.c_RWave.r_wave)
& c_MeasuredParameters.c_RWave.r_wave = 0);