Verifiable code

[R. T. (Fortran Man)]

What is the difference between verifiable and non-verifiable code?

[Lahey Support]

Verification of code involves subjecting it to stringent tests to determine whether the code is type safe, and to ensure that the code does not access memory or resources to which it has not been granted access.

A mathematical definition of verifiability has been developed, and this definition is applied to code to determine it’s verifiability. The mathematical definition is quite strict, and so all code that is type safe is not necessarily verifiable.

Type safety provides an assurance that variables of one type will not masquerade as another type, that operations that are not appropriate to a variable type will not be applied to that type, and that a variable will only access memory to which it has been granted access.

Not all Fortran code can result in type safe or verifiable code. For example, code that equivalences different variable types, or contains mismatched calling interfaces or common blocks will not be type safe or verifiable. Where possible, Fortran for .NET always produces verifiable code. When Fortran constructs are used that are not inherently verifiable, the compiler will produce non-verifiable code.

Verification essentially provides a guarantee that programs will act in a predictable. It provides an assurance that code being downloaded, either as an executable or in a web browser will run within the security guidelines on a given machine.