Information Technology Reference
In-Depth Information
behavior no_forced_brake_necessary:
assumes loc->standstill || (!loc->standstill &&
!vig_button_hold_expired(vig, loc) &&
!vig_button_break_expired(vig, loc));
assigns \nothing;
complete behaviors;
disjoint behaviors;
*
/
void process_vigilance_device(Vigilance_device
*
vig, Locomotive
*
loc);
Since the function contains pointers that must be dereferenceable, we use
the
\valid
clause to specify this requirement. We include our user-defined
predicates
vigilance_invariant
and
locomotive_invariant
as pre- and
postconditions into the function contract in order to emulate type invariants.
Additionally, we expect the formerly defined predicate
actual_time_is_latest_time
to hold as pre- and as postcondition, which
means no time variable may have values describing the future relative to the
actual time.
At the end of that contract we can specify that the described behaviors are
complete
and
disjoint
, as they include all possibilities and both exclude
each other. The inclusion of these last clauses provides an additional check
on the specification itself.
4
Implementation
Below, the implementation of the function formally specified in the former
subsection is depicted. Given the very precise formal specification, the imple-
mentation of this function is straightforward.
void process_vigilance_device(Vigilance_device
*
vig, Locomotive
*
loc) {
if (!loc->standstill){
if (check_vig_button_break_expired(vig, loc) {
loc->train_brake = TRUE;
loc->forced_brake = TRUE;
}
else if (check_vig_button_hold_expired(vig, loc)) {
loc->train_brake = TRUE;
loc->forced_brake = TRUE;
}
}
}
This function calls two auxiliary functions:
int check_vig_button_hold_expired(Vigilance_device
*
vig, Locomotive
*
loc);
int check_vig_button_break_expired(Vigilance_device
*
vig, Locomotive
*
loc);
Each of those, of course, must be formally specified as well. This example
shows, that the programmer needs to have knowledge about the specification
language as well. This process is comparable to the fact, that the programmer
must also be able to write unit tests.
