1 |
Note that the proofs of correctness do not constitute proof that the implementation
of the medrina package is correct; the implementation code is manually translated
from the specification code, and this allows for human error in the transcription and the possibility of
differing semantics of the execution environment. The specification itself is intended to provide an unambiguous
description of the behaviour that an implementation should have, and the proofs of
correctness are intended to demonstrate the absence of design flaws in the system as specified.
References to this footnote:
1
|