Skip to content

A simple yet slightly non-obvious assertion utility for Fortran 2018

License

Notifications You must be signed in to change notification settings

sourceryinstitute/assert

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

85 Commits
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

Assert

A simple assertion utility taking advantage of the Fortran 2018 standard's introduction of variable stop codes and error termination inside pure procedures.

Motivations

  1. To mitigate against a reason developers often cite for not writing pure procedures: their inability to produce output in normal execution.
  2. To promote the enforcement of programming contracts.

Overview

This assertion utility contains three public entities:

  1. An assert subroutine,
  2. A characterizable_t abstract type supporting assert, and
  3. An intrinsic_array_t non-abstract type extending characterizable_t.

The assert subroutine

  • Error-terminates with a variable stop code when a user-defined logical assertion fails,
  • Includes user-supplied diagnostic data in the output if provided by the calling procedure,
  • Is callable inside pure procedures, and
  • Can be eliminated during an optimizing compiler's dead-code removal phase based on a preprocessor macro: -DUSE_ASSERTIONS=.false..

The characterizable_t type defines an as_character() deferred binding that produces character strings for use as diagnostic output from a user-defined derived type that extends characterizable_t and implements the deferred binding.

The intrinsic_array_t type that extends characterizable_t provides a convenient mechanism for producing diagnostic output from arrays of intrinsic type complex, integer, logical, or real.

Documentation

See Assert's GitHub Pages site for HTML documentation generated with ford.

Use Cases

Two common use cases include

  1. Enforcing programming contracts throughout a project via runtime checks.
  2. Producing output in pure procedures for debugging purposes.

Enforcing programming contracts

Programming can be thought of as requirements for correct execution of a procedure and assurances for the result of correct execution. The requirements and assurances might be constraints of three kinds:

  1. Preconditions (requirements): logical expressions that must evaluate to .true. when a procedure starts execution,
  2. Postconditions (assurances): expressions that must evaluate to .true. when a procedure finishes execution, and
  3. Invariants: universal pre- and postconditions that must always be true when all procedures in a class start or finish executing.

The [examples/README.md] file shows examples of writing constraints in notes on class diagrams using the formal syntax of the Object Constraint Language (OCL).

Downloading, Building, and Running Examples

Prerequisites

  1. A Fortran 2018 compiler.
  2. The Fortran Package Manager.
  3. Optional: OpenCoarrays for parallel execution with the GNU Fortran compiler.

Assert was developed primarily with gfortran 11.2.0 and nagfor 7.1. Recent versions of the Cray and Intel compilers should also suffice.

Downloading Assert

git clone [email protected]:sourceryinstitute/assert
cd assert

Building and testing with gfortran

Single-image (serial) execution

The following command builds Assert and runs the full test suite in a single image:

fpm test

where fpm test builds the Assert library and runs the test suite, including the tests.

Multi-image (parallel) execution

With gfortran and OpenCoarrays installed,

fpm test --compiler caf --runner "cafrun -n 2"

To build and test with the Numerical Algorithms Group (NAG) Fortran compiler version 7.1 or later, use

fpm test --compiler=nagfor --flag="-coarray=cosmp -fpp -f2018"

Building and testing with the Intel ifx compiler

fpm test --compiler ifx --flag -coarray

Building and testing with the Numerical Algorithms Group (NAG) compiler

fpm test --compiler nagfor --flag "-fpp -coarray=cosmp"

Building and testing with the Cray Compiler Environment (CCE)

Because fpm uses the compiler name to determine the compiler identity and because CCE provides one compiler wrapper, ftn, for invoking all compilers, you will need to invoke ftn in a shell script named to identify CCE compiler. For example, place a script named crayftn.sh in your path with the following contents and with executable privileges set appropriately:

#!/bin/bash

ftn $@

Then build and test Assert with the command

fpm test --compiler crayftn.sh

Building and testing with other compilers

To use Assert with other compilers, please submit an issue or pull request.

Running the examples

See the ./example subdirectory.

Documentation

For further documentation, please see example/README.md and the tests. Also, the code in src has comments formatted for generating HTML documentation using FORD.