ISO/IEC TR 15942:2000

TECHNICAL ISO/IEC
REPORT TR
First edition
2000-03-01
Information technology — Programming
languages — Guide for the use of the Ada
programming language in high integrity
systems
Technologies de l'information — Langages de programmation — Guide
pour l'emploi du langage de programmation Ada dans les systèmes de
haute intégrité
Reference number
©
ISO/IEC 2000
PDF disclaimer
This PDF file may contain embedded typefaces. In accordance with Adobe's licensing policy, this file may be printed or viewed but shall not
be edited unless the typefaces which are embedded are licensed to and installed on the computer performing the editing. In downloading this
file, parties accept therein the responsibility of not infringing Adobe's licensing policy. The ISO Central Secretariat accepts no liability in this
area.
Adobe is a trademark of Adobe Systems Incorporated.
Details of the software products used to create this PDF file can be found in the General Info relative to the file; the PDF-creation parameters
were optimized for printing. Every care has been taken to ensure that the file is suitable for use by ISO member bodies. In the unlikely event
that a problem relating to it is found, please inform the Central Secretariat at the address given below.
© ISO/IEC 2000
All rights reserved. Unless otherwise specified, no part of this publication may be reproduced or utilized in any form or by any means, electronic
or mechanical, including photocopying and microfilm, without permission in writing from either ISO at the address below or ISO's member body
in the country of the requester.
ISO copyright office
Case postale 56 � CH-1211 Geneva 20
Tel. + 41 22 749 01 11
Fax + 41 22 734 10 79
E-mail copyright@iso.ch
Web www.iso.ch
Printed in Switzerland
ii © ISO/IEC 2000 – All rights reserved

Contents
1 Scope.1
1.1 Within the scope.1
1.2 Out of scope .2
2 Verification Techniques .2
2.1 Traceability .2
2.2 Reviews .3
2.3 Analysis.3
2.3.1 Control Flow analysis .4
2.3.2 Data Flow analysis .4
2.3.3 Information Flow analysis .4
2.3.4 Symbolic Execution .4
2.3.5 Formal Code Verification.5
2.3.6 Range Checking .6
2.3.7 Stack Usage analysis.6
2.3.8 Timing Analysis.6
2.3.9 Other Memory Usage analysis.6
2.3.10 Object Code Analysis .7
2.4 Testing.7
2.4.1 Principles .7
2.4.2 Requirements-based Testing.7
2.4.3 Structure-based Testing.8
2.5 Use of Verification Techniques in this Technical Report.8
3 General Language Issues .9
3.1 Writing Verifiable Programs .9
3.1.1 Language Rules to Achieve Predictability.10
3.1.2 Language Rules to Allow Modelling.10
3.1.3 Language Rules to Facilitate Testing.11
3.1.4 Pragmatic Considerations.12
3.1.5 Language Enhancements.12
3.2 The Choice of Language.13
4 Significance of Language Features for High Integrity.14
4.1 Criteria for Assessment of Language Features .14
4.2 How to use this Technical Report .14
5 Assessment of Language Features.15
5.1 Types with Static Attributes.16
5.1.1 Evaluation .17
5.1.2 Notes .17
5.1.3 Guidance .17
5.2 Declarations.17
5.2.1 Evaluation .18
5.2.2 Notes .18
5.2.3 Guidance .18
5.3 Names, including Scope and Visibility.19
5.3.1 Evaluation .19
5.3.2 Notes .19
5.3.3 Guidance .20
5.4 Expressions .20
5.4.1 Evaluation .21
5.4.2 Notes .21
5.4.3 Guidance .22
iii
© ISO/IEC 2000 - All rights reserved

5.5 Statements.22
5.5.1 Evaluation .23
5.5.2 Notes .23
5.5.3 Guidance.23
5.6 Subprograms.24
5.6.1 Evaluation .24
5.6.2 Notes .24
5.6.3 Guidance.25
5.7 Packages (child and library) .25
5.7.1 Evaluation .26
5.7.2 Notes .26
5.7.3 Guidance.26
5.8 Arithmetic Types .27
5.8.1 Evaluation .27
5.8.2 Notes .27
5.8.3 Guidance.28
5.9 Low Level and Interfacing.29
5.9.1 Evaluation .30
5.9.2 Notes .30
5.9.3 Guidance.31
5.10 Generics.31
5.10.1 Evaluation .32
5.10.2 Notes .32
5.10.3 Guidance.33
5.11 Access Types and Types with Dynamic Attributes .34
5.11.1 Evaluation .34
5.11.2 Notes .34
5.11.3 Guidance.35
5.12 Exceptions .35
5.12.1 Evaluation .36
5.12.2 Notes .36
5.12.3 Guidance.36
5.13 Tasking.37
5.13.1 Evaluation .39
5.13.2 Notes .39
5.13.3 Guidance.39
5.14 Distribution .40
5.14.1 Evaluation .40
5.14.2 Notes .40
5.14.3 Guidance.40
6 Compilers and Run-time Systems .40
6.1 Language issues .41
6.2 Compiler Qualification.41
6.3 Run-Time System.42
7 References .43
7.1 Applicable Documents .43
7.2 Referenced Documents .44
iv © ISO/IEC 2000 - All rights reserved

Foreword
ISO (the International Organization for Standardization) and IEC (the International Electrotechnical Commission) form the
specialized system for worldwide standardization. National bodies that are members of ISO or IEC participate in the
development of International Standards through technical committees established by the respective organization to deal with
particular fields of technical activity. ISO and IEC technical committees collaborate in fields of mutual interest. Other
international organizations, governmental and non-governmental, in liaison with ISO and IEC, also take part in the work.
International Standards are drafted in accordance with the rules given in the ISO/IEC Directives, Part 3.
In the field of information technology, ISO and IEC have established a joint technical committee, ISO/IEC JTC 1. Draft
International Standards adopted by the technical committees are circulated to the member bodies for voting. Publication as an
International Standard requires approval by at least 75 % of the member bodies casting a vote.
In exceptional circumstances, when a technical committee has collected data of a different kind from that which is normally
published as an International Standard ("state of the art", for example), it may decide by a simple majority vote of its
participating members to publish a Technical Report. A Technical Report is entirely informative in nature and does not have to
be reviewed until the data it provides are considered to be no longer valid or useful.
Attention is drawn to the possibility that some of the elements of this Technical Report may be the subject of patent rights. ISO
and IEC shall not be held responsible for identifying any or all such patent rights.
ISO/IEC TR 15942 was prepared by Joint Technical Committee ISO/IEC JTC 1, Information technology, Subcommittee
SC 22, Programming languages, their environments and system software interfaces.
v
© ISO/IEC 2000 - All rights reserved

Introduction
As a society, we are increasingly reliant upon high integrity systems: for safety systems (such as fly-by-wire aircraft), for
security systems (to protect digital information) or for financial systems (e.g., cash dispensers). As the complexity of these
systems grows, so do the demands for improved techniques for the production of the software components of the system.
These high integrity systems must be shown to be fully predictable in operation and have all the properties required of them.
This can only be achieved by analysing the software, in addition to the use of conventional dynamic testing.
There is, currently, no mainstream high level language where all programs in that language are guaranteed to be predictable and
analysable. Therefore for any choice of implementation language it is essential to control the ways that the language is used by
the application.
The Ada language [ARM] is designed with specific mechanisms for controlling the use of certain aspects of the language.
Furthermore,
1. The semantics of Ada programs are well-defined, even in error situations. Specifically, the effect of a program
can be predicted from the language definition with few implementation dependencies or interactions between
language features.
2. The strong typing within the language can be used to reduce the scope (and cost) of analysis to verify key
properties.
3. The Ada language has been successfully used on many high integrity applications. This demonstrates that
validated Ada compilers have the quality required for such applications.
4. Guidance can be provided to facilitate the use of the language and to encourage the development of tools for
further verification.
Ada is therefore ideally suited for implementing high integrity software and this document provides guidance in the controls
that are required on the use of Ada to ensure that programs are predictable and analysable.
All language design balances functionality against integrity. For instance, the ability to control storage allocation directly will
impact the need to ensure the integrity of data. An aspect of the integrity of Ada programs is the possibility of avoiding access
types (references) completely, whereas in other languages references are linked to array accessing and/or parameter passing,
and therefore cannot be excluded.
There are a number of different analysis techniques in use for high integrity software and this document is not prescriptive
about which techniques to use. Furthermore, each analysis technique requires different controls on the use of the language. Ada
assists analysis: for instance, the modes of Ada parameters, suitably used, provide information for data flow analysis which
other languages cannot always provide. This Technical Report, therefore, catalogues specific verification techniques (see 2.5),
and classifies the impact that language features have on the use of these techniques (in the tables in Section 5).
It is the user's responsibility to select the analysis techniques for a particular application; this document can then be used to
define the full set of controls necessary for using that set of techniques.
The guidance given here first specifies its scope, by reference to the safety and security standards to which high integrity
applications may be written.
Section 2 then analyses the verification techniques that are applied in the development of high integrity systems. By this
means, the regulatory rules of the standards for safety and security are abstracted to avoid the need to consider each such
standard separately.
Section 3 addresses general issues concerning how computer languages must be constructed if programs written in that
language are to be fully predictable. These issues are relevant to any restricted language defined through the application of this
guidance.
vi © ISO/IEC 2000 - All rights reserved

Section 4 provides identification of a three-way classification system used for Ada language features. This classification is
based upon the ease with which verification techniques can be applied to a program containing the feature. This classification
is needed since while the majority of the core features in Ada assists verification, the use of certain features makes the resulting
code difficult or impossible to analyse with the currently available program analysis tools and techniques.
Section 5 provides the main technical material of this Technical Report by classifying Ada language features. Users of this
Technical Report can then determine which features of Ada are appropriate to use from the verification techniques that are to
be employed. The assessment has shown that the vast majority of the Ada features lend themselves to effective use in the
construction of high integrity systems.
The Technical Report concludes, in Section 6, by providing information to aid the choice of a suitable Ada compiler together
with its associated run-time system.
References to relevant standards and guides are provided. A detailed analysis of Ada95 for high integrity systems is available
in References [CAT1, CAT2] and [CAT3] .
A comprehensive index is provided to ease the use of the Technical Report.
Levels of criticality
Many of the Standards to which high integrity software is written use multiple levels to classify the criticality of the software
components which make up the system. While the number and nature of the levels vary, the general approach is always the
same: the higher the criticality of the system, the more verification techniques need to be used for its assurance. Table 1 relates
the various levels of classification used in some well known International Standards.
Table 1: Levels of criticality in some Standards
Standard Number of levels Lowest Level Highest Level
[DO-178B] 4 D A
[IEC-61508] 4 Safety Integrity Level 1 Safety Integrity Level 4
[ITSEC] 7 E0 E6
This Technical Report emphasizes the higher levels of criticality, for which the more demanding verification techniques are
employed and for which Ada provides major benefits.
This Technical Report, however, does not directly use any such levels but focuses on the correlation between the features of the
language and the verification techniques to be employed at the higher levels of criticality. The material in [ISO/IEC 15026],
[DS 00-56], [ARP 4754] and [ARP 4761] may be useful in determining the criticality of a system if this is not covered by
application-specific standards.
Readership
This Technical Report has been written for:
1. Those responsible for coding standards applicable to high integrity Ada software.
2. Those developing high integrity systems in Ada.
3. Vendors marketing Ada compilers, source code generators, and verification tools for use
in the development of high integrity systems.
4. Regulators who need to approve high integrity systems containing software written in
Ada.
5. Those concerned with high integrity systems who wish to consider the advantages of
using the Ada language.
This Technical Report is not a tutorial on the use of Ada or on the development of high integrity software. Developers using
this report are assumed to have a working knowledge of the language and an understanding of good Ada style, as in [AQS].
vii
© ISO/IEC 2000 - All rights reserved

History
When proposals were made that a subset of Ada should be specified for high integrity applications, it was realized that the
provision of the Safety and Security Annex in the Ada standard did not satisfy all the requirements of the developers of high
integrity systems. In consequence, a group was formed under WG9 to consider what action was needed. This group, called the
HRG, proposed and drafted this Technical Report over a three year period.
Conventions
In line with the Ada standard, the main text is in a Roman font. Ada identifiers are set in a sans-serif font, and the Ada
keywords in a bold sans-serif font.
Postscript
The guidance provided here reflects the understanding of the issues based mainly on using the previous Ada standard in
developing high integrity applications. Over the next few years, the current Ada standard will be used for further high integrity
applications which will no doubt need to be reflected in a revision of this guidance. Specifically, further detail can be produced
based upon the experience gained.
Instructions for comment submission
Informal comments on this Technical Report may be sent by e-mail to hrg@cise.npl.co.uk. If appropriate, the project editor will
document the issue for corrective action.
Comments should use the following format:
!topic: Title which is a summary in one sentence
!reference TR 15942- ss.ss.ss
!from Author, Name, yy-mm-dd
!keywords keywords related to topic
!discussion
text of discussion
where ss.ss.ss is the section number, yy-mm-dd is the date. If the comment requests a change, a rationale for this and the
substance of the actual change proposed would facilitate the processing of the comment.
viii © ISO/IEC 2000 - All rights reserved

TECHNICAL REPORT
Information technology - Programming languages - Guide for the
use of the Ada programming language in high integrity systems
1 Scope
This Technical Report provides guidance on the use of Ada when producing high integrity systems. In producing such
applications it is usually the case that adherence to guidelines or standards has to be demonstrated to independent bodies.
These guidelines or standards vary according to the application area, industrial sector or nature of the risk involved.
For safety applications, the international generic standard is [IEC 61508] of which part 3 is concerned with software.
For security systems, the multi-national generic assessment guide is [ISO CD 15408].
For sector-specific guidance and standards there are:
Airborne civil avionics: [DO-178B]
Nuclear power plants: [IEC 880]
Medical systems: [IEC 601-4]
Pharmaceutical:[GAMP]
For national/regional guidance and standards there are the following:
UK Defence: [DS 00-55]
European rail: [EN 50128]
European security:[ITSEC]
US nuclear:[NRC]
UK automotive:[MISRA]
US medical:[FDA]
US space:[NASA]
The above standards and guides are referred to as Standards in this Technical Report. The above list is not exhaustive but
indicative of the type of Standard to which this Technical Report provides guidance.
The specific Standards above are not addressed individually but this Technical Report is synthesized from an analysis of their
requirements and recommendations.
1.1 Within the scope
This Technical Report assumes that a system is being developed in Ada to meet a standard listed above or one of a similar
nature. The primary goal of this Technical Report is to translate general requirements into Ada specific ones. For example, a
general standard might require that dynamic testing provides evidence of the execution of all the statements in the code of the
application. In the case of generics, this is interpreted by this Technical Report to mean all instantiations of the generic should
be executed.
© ISO/IEC 2000 - All rights reserved 1

This Technical Report is intended to provide guidance only, and hence there are no ‘shalls’. However, this Technical Report
identifies verification and validation issues which should be resolved and documented according to the sector-specific
standards being employed.
The following topics are within the scope of this Technical Report:
� the choice of features of the language which aid verification and compliance to the standards,
� identification of language features requiring additional verification steps,
� the use of tools to aid design and verification,
� issues concerning qualification of compilers for use on high integrity applications,
� tools, such as graphic design tools, which generate Ada source code which is accessible to users.
Tools which generate Ada source code require special consideration. Where generated code may be modified or extended,
verification of the extensions and overall system will be assisted if the guidelines have been taken into account. Even where
modification is not planned, inspection and analysis of the generated code may be unavoidable unless the generator is trusted or
‘qualified’ according to an applicable standard. Finally, even if generated code is neither modified nor inspected, the overall
verification process may be made more complicated if the code deviates from guidelines intended to facilitate testing and
analysis. Potential users of such tools should evaluate their code generation against the guidance provided in this Technical
Report.
1.2 Out of scope
The following topics are considered to be out of scope with respect to this Technical Report:
� Domain-specific standards,
� Application-specific issues,
� Hardware and system-specific issues,
� Human factor issues in the application (as opposed to human factors in the use of the Ada language which is in
scope).
2 Verification Techniques
Verification is the confirmation by examination and provision of objective evidence that specified requirements have been
fulfilled [ISO 8402: 2.18] .
There are currently four approaches required by applicable standards and guidelines (see Section 7.1) to support the
verification of software:
1. traceability,
2. reviews,
3. analysis, and
4. testing.
Each one of these is discussed below. Where appropriate, language-specific techniques that support each approach are
discussed. Finally, these techniques are grouped into categories that can form a basis for the analysis of Ada language features.
This analytical approach forms the basis for the assessment presented in Section 5.
2.1 Traceability
Traceability is required to establish that the implementation is complete, and to identify new derived requirements. It occurs
throughout the life cycle, e.g., there needs to be traceability from:
2 © ISO/IEC 2000 - All rights reserved

� lower level (decomposed) requirements to higher level requirements;
� test procedures to requirements, design, or code;
� object code to source code.
While traceability is not language specific, certain attributes of design or coding styles can aid in (or detract from)
accomplishing this objective. For example, consider a single module that implements a single low level requirement, which has
an associated single test procedure, then the method to support traceability is straightforward. On the other hand, if there is a
many-to-many relationship between the various decomposed levels of software (because of design choices or test procedures),
traceability can become very complicated. Deduction of completeness of implementation (without extraneous code) may
therefore be difficult or impossible.
Additionally, the use of some of the more sophisticated language features of high-level languages that require extensive
compiler generated code may detract from the straightforward translation into, and hence traceability of, the object code.
2.2 Reviews
Reviews are an important part of the verification process. They can be carried out on requirements, design, code, test
procedures, or analysis reports. Reviews are conducted by humans and may be undertaken ‘formally’ such as in a Fagan
inspection [11] or ‘informally’ such as in desk checks. Typically, reviews are done by an ‘independent’ person i.e., the
producer of the artefact is different from the reviewer. This independence is a mandatory requirement of safety-critical
software standards.
Coding standards and avoidance of certain language features of high-level languages are essential for high integrity systems in
order to facilitate reviews. These aspects become important since the ‘independent’ code review may at times be conducted by
an expert in the application domain who may not have detailed insight into language constructs and their interactions.
There is a distinct tradeoff between the use of language features to capture design intent and support abstraction versus the need
for simplicity and predictability. This document leaves to coding guidelines, such as the Ada Quality and Style Guide [AQS],
software engineering issues such as those concerned with readability and reusability. Those issues that are associated with
quantifiable analysis are considered in the following sections.
2.3 Analysis
This Technical Report distinguishes between analysis (i.e., static analysis) and testing (i.e., dynamic analysis). Analysis
supplements testing to establish that the requirements are correctly implemented.
Analysis can be performed on requirements, design, or code; the major emphasis of this Technical Report is the analysis of the
design and code.
Described below are ten analysis methods which are required in different combinations by various standards.
1. Control Flow
2. Data Flow
3. Information Flow
4. Symbolic Execution
5. Formal Code Verification
6. Range Checking
7. Stack Usage
8. Timing Analysis
9. Other Memory Usage
10. Object Code Analysis
© ISO/IEC 2000 - All rights reserved 3

2.3.1 Control Flow analysis
Control Flow analysis is conducted to
1. ensure that code is executed in the right sequence,
2. ensure that code is well structured,
3. locate any syntactically unreachable code, and
4. highlight the parts of the code where termination needs to be considered, i.e., loops and recursion.
Call tree analysis, an example of one of the many Control Flow analysis techniques available, is used to verify that the
sequencing stated by the design is correctly implemented. Also, call tree analysis can help detect direct and indirect recursion,
which are prohibited by most high integrity standards. Furthermore, if a system is partitioned into critical and non-critical parts,
then the call tree analysis can confirm that the design rules for partitioning have been followed.
Ada is rich in facilities for program flow control. Language rules, such as prohibition of modification of for loop control
variables, make it difficult to produce poorly structured Ada code. If the goto statement is not used and relatively minor
restrictions are made on placement of exit and return statements, Ada code becomes inherently well structured.
2.3.2 Data Flow analysis
The objective of Data Flow analysis is to show that there is no execution path in the software that would access a variable that
has not been set a value. Data Flow analysis uses the results of Control Flow Analysis in conjunction with the read or write
access to variables to perform the analysis. Data Flow analysis can also detect other code anomalies such as multiple writes
without intervening reads.
In most general-purpose languages, Data Flow analysis is a complex activity, mainly because global variables can be accessed
from anywhere, and because subprogram parameters do not support out-only modes. The job can be made significantly easier
in Ada which has packages to contain potentially shared data, and out mode parameters on subprograms.
2.3.3 Information Flow analysis
Information Flow analysis identifies how execution of a unit of code creates dependencies between the inputs to and outputs
from that code. For example:
X := A+B;
Y := D-C;
if X>0 then
Z:=(Y+1);
end if;
Here, X depends on A and B, Y depends on C and D,and Z depends on A, B, C,and D (and implicitly on its own initial value).
These dependencies can be verified against the dependencies in the specification to ensure that all the required dependencies
are implemented and no incorrect ones are established. It can be performed either internal to a module (i.e., a procedure or a
function), across modules, or across the entire software (or system). This analysis can be particularly appropriate for a critical
output that can be traced back all the way to the inputs of the hardware/software interface.
2.3.4 Symbolic Execution
The objective of Symbolic Execution is to verify properties of a program by algebraic manipulation of the source text without
requiring a formal specification. This technique is typically applied using tools that also undertake Control Flow, Data Flow
and Information Flow analysis.
Symbolic Execution is a technique where the program is ‘executed’ by performing back-substitution; in essence, the right hand
side of each assignment is substituted for the left hand side variable in its subsequent uses. This converts the sequential logic
into a set of parallel assignments in which output values are expressed in terms of input values. Conditional branches are
represented as conditions under which the relevant expression gives the values of the outputs from the inputs. To undertake this
4 © ISO/IEC 2000 - All rights reserved

computation, it is assumed that no aliasing is taking place, i.e., two variables X and Y do not refer to the same entity and that
functions have no side-effects. Tools that provide support for symbolic execution may or may not check for these conditions.
Using the fragment of Ada code which illustrated Information Flow analysis gives:
A+B � 0:
X = A+B
Y = D-C
Z = not defined on this path (retains initial value)
A+B >0:
X = A+B
Y = D-C
Z = D-C+1
These algebraic expressions give the output in terms of the input and can be compared (manually) with the specification of a
subprogram to verify the code.
Symbolic Execution can also be used to assist with reasoning that run-time errors will not occur (e.g., Range Checking). The
Symbolic Execution model is extended to include expressions indicating the conditions under which a run-time error may
occur. If these expressions are mutually contradictory for a particular execution path then that path is free from potential run-
time errors. In the above example, if Z has an upper declared bound of 10, then we have the condition that if A+B>0, then D-
C+1<11 to avoid raising the exception on the upper bound.
2.3.5 Formal Code Verification
Formal Code Verification is the process of proving that the code of a program is correct with respect to the formal specification
of its requirements. The objective is to explore all possible program executions, which is infeasible by dynamic testing alone.
Each program unit is verified separately, against those parts of the specification that apply to it. For instance, Formal Code
Verification of a subprogram involves proving that its code is consistent with its formally-stated post-condition (specifying the
intended relationships between variables on termination), given its pre-condition (specifying the conditions which must apply
when the subprogram is called). A more restricted proof aimed at demonstrating a particular safety/security property can also
be constructed.
The verification is usually performed in two stages:
1. Generation of Verification Conditions (VCs). These theorems are proof obligations, whose truth implies that if
the pre-condition holds initially, and execution of the code terminates, then the post-condition holds on
termination. These VCs are usually generated mechanically.
2. Proof of VCs. Machine assistance in the form of a suitable proof tool can be used to discharge verification
conditions.
The process outlined above establishes partial correctness. To establish total correctness it is also necessary to prove
termination of all loops when the stated pre-condition holds and termination of any recursion. Recursion is not normally
permitted in high integrity systems. Termination is usually demonstrated by exhibiting a variant expression for every loop, and
showing that this expression gives a non-negative number that decreases on each iteration. Termination conditions can be
generated and proved, similarly to the generation and proof of verification conditions.
The value of Formal Code Verification depends on the availability of a specification expressed in a suitable form such as
results from formal specification methods. Formal methods involve the use of formal logic, discrete mathematics, and
computer-readable languages to improve the specification of software.
Proof of absence of run-time errors
In some real-time high integrity systems, occurrence of run-time errors is not acceptable. An example is the flight-control
system of a dynamically unstable aircraft, in which there would not be time to recover from such an error. The techniques of
Formal Code Verification described above can be used to prove that (with appropriate language constraints) certain classes of
run-time errors, e.g., range constraint violations, cannot arise in any execution.
To perform such verifications, the object type and variable declarations are used to construct pre-conditions on the ranges of
initial values, and at each place in the source code where a run-time check would be produced, an assertion formally describing
© ISO/IEC 2000 - All rights reserved 5

the check is generated. From these pre-conditions, assertions and the program code, verification conditions are mechanically
produced.
These verifications (or ‘proof obligations’) are numerous, but for the most part simple enough to be proved automatically. Full
formal requirement specifications are n
...