In all VDM dialects, you can identify places where run-time errors could potentially occur if the model was to be executed. The analysis of these areas can be considered as a complement to the static type checking that is performed automatically. Type checking accepts possibly correct specifications, but we also want to know the places where the specification could fail.

Unfortunately, it is not always possible to statically check if such potential problems will occur at run-time. To overcome this issue we can generate Proof Obligations (POs) for all the places where run-time errors could occur. Each PO is formulated as a predicate that must hold at a particular place in the VDM model if it is error-free, and so it may have particular context information associated with it. POs can be considered as constraints that will guarantee the internal integrity of a VDM model, if they are all met.

In the future, it will be possible to automatically prove these constraints with a proof component in the IDE, but this is not yet available. Until then, each PO has a fixed "Status" that is either Proved or Unproved. Trivial POs can be proved immediately, as they are generated, but more complex Unproved obligations would require a theorem prover to discharge them.

The Proof Obligation View

The proof obligation generator is invoked either on a VDM project (and then POs for all the VDM model files will be generated) or for one selected VDM file. Right-click the file in the Explorer and then select Run Proof Obligation Generation. VS Code will open a special Proof Obligation view.

Once you have generated POs for a VDM project for the first time, they will automatically be re-generated whenever the project is rebuilt as long as you stay in the Proof Obligations view.

In this view, all the information about the proof obligations is displayed and several options are available to sort the proof obligations. You can also quickly navigate to the location in the specification that is responsible for the proof obligation by double-clicking a proof obligation. You can expand or collapse all POs with the buttons Expand all proof obligations and Collapse all proof obligations, and you can filter the POs using Filter by status.

Note that in the Proof Obligation View, each proof obligation has four components:

• ID: A unique number for that PO
• Kind: The PO type
• Name: The name of the definition in which the proof obligation is located
• Status: The proof status of the PO - trivial POs may be Proved but others will be Unproved

Categories of Obligation

POs can be divided into different categories depending upon their nature. This is marked in the table as the PO Kind. They are listed here in alphabetical order:

Kind	Description
cases exhaustive	If a cases expression does not have another clause it is necessary to ensure that the different case alternatives catch all values of the type of expression used in the case choice.
equivalence relation	An obligation requiring types that define eq to be an equivalence relation
finite map	If a type binding to a type that potentially has infinitely many elements is used inside a map comprehension, this proof obligation will be generated because all mappings in VDM must be finite.
finite set	If a type binding to a type that potentially has infinitely many elements is used inside a set comprehension, this proof obligation will be generated because all sets in VDM must be finite.
function apply	Whenever a function application is used you need to be certain that the list of arguments to the function satisfies the pre-condition of the function, assuming such a predicate is present.
function compose	When using a function composition (f comp g), this ensures that the precondition of g implies the precondition off applied to the result of g.
function iteration	When using a function iteration, for the function we are iterating with, this ensures that the precondition on an argument implies the precondition on the result.
function parameter patterns	When using a pattern as a function parameter, this ensures that all values in the parameter type for the function can match the pattern.
function postcondition satisfiable	Whenever a function has a postcondition this checks that the precondition of the function implies the postcondition.
function satisfiability	For all implicit function definitions this proof obligation will be generated to ensure that it is possible to find an implementation satisfying the post-conditions for all arguments satisfying the pre-conditions.
map apply	Whenever a map application is made you need to be certain that the argument is in the domain of the map.
invariant satisfiability	Proof obligations from this category are used to ensure that type and state invariants are satisfiable
let be st existence	Whenever a let-be-such-that expression/statement is used you need to be certain that at least one value will match the such-that expression.
map compose	When composing 2 maps, ensure that the range of map2 is a subset of the domain of map1.
map compatible	Mappings in VDM represent a unique relationship between the domain values and the corresponding range values. Proof obligations in this category are meant to ensure that such a unique relationship is guaranteed.
map iteration	When performing a map iteration, ensure the iteration count expression is either 0 or 1 or if it’s greater than 1 then the map’s range is a subset of its domain.
map sequence compatible	When defining a map with enumeration, ensures that any two equal elements in the domain map to the same element in the range.
map set compatible	When merging a set of maps, any two equal elements in the domains of each map map to the same element in the range.
non-empty sequence	This kind of proof obligation is used whenever non-empty sequences are required (eg. taking the head of a sequence)
non-empty set	This kind of proof obligation is used whenever non-empty sets are required.
non-zero	This kind of proof obligation is used whenever zero cannot be used (e.g. in division).
operation parameter patterns	When using a pattern as an operation parameter ensures that all values in the operation parameter type can match the pattern.
operation post condition	Whenever an explicit operation has a post-condition there is an implicit proof obligation generated to remind the user that you have to ensure that the explicit body of the operation satisfies the post-condition for all possible inputs.
operation satisfiability	For all implicit operation definitions this proof obligation will be generated to ensure that it is possible to find an implementation satisfying the post-condition for all arguments satisfying the pre-conditions.
ordered	When comparing unions of types, there must be pairs of LHS/RHS types that are comparable
recursive function	This proof obligation makes use of the measure construct to ensure that a recursive function will terminate.
sequence apply	Whenever a sequence application is used you need to be certain that the argument is within the indices of the sequence.
sequence modification	Whenever a sequence modification is used, this ensures the domain of the modification map is a subset of the indices of the sequence.
set membership	To check that a value is a member of a set
seq membership	To check that a value is a member of a sequence
state init	An obligation requiring a state initializer to be satisfiable
state invariant	If a state (including instance variables in VDM++) has an invariant, this proof obligation will be generated whenever an assignment is made to a part of the state.
strict order	And obligation that requires a type with an ord clause to implement a strict order
subtype	This proof obligation category is used whenever it is not possible to statically detect that the given value falls into the subtype required.
total function	An obligation requiring total functions to define results for all arguments
tuple selection	This proof obligation category is used whenever a tuple selection expression is used to guarantee that the length of the tuple is at least as long as the selector used.
type compatibility	Proof obligations from this category are used to ensure that when constructing values of types that have an invariant live up to that invariant.
unique existence binding	The iota expression requires one unique binding to be present and that is guaranteed by proof obligations from this category.
value binding	When binding a value to a pattern, ensure that the resulting value matches the pattern.
while loop termination	This kind of proof obligation is a reminder to ensure that a while loop will terminate.

Further Reading

• [1] Proof in VDM, Juan C. Bicarregui et. al.
• [2] SYSTEMATIC SOFTWARE DEVELOPMENT USING VDM, 2nd Edition, Cliff B. Jones
• [3] The VDM Language Board working group on proof obligations. See here.