Download citation
Download citation
link to html
An application of formal verification (using the proof assistant Isabelle/HOL) for ensuring the correctness of scientific data processing software in the crystallographic domain is presented. The proposed process consists of writing a pseudocode that describes an algorithm in a succinct but mathematically unambiguous way, then formulating or reusing necessary Isabelle theories and proving algorithm properties within these theories, and finally implementing the algorithm in a practical programming language. Both the formal proof and the semi-formal algorithm analysis are demonstrated on an example of a simple but important algorithm (widely used in crystallographic computing) that reconstructs a space-group operator list from a subset of symmetry operators. The cod-tools software package that implements the verified algorithm is also presented. On the basis of the reported results, it is argued that broader application of formal methods (e.g. formal verification of algorithm correctness) allows developers to improve the reliability of scientific software. Moreover, the formalized (within the proof assistant) domain-specific theory can be reused and gradually extended, thus continuously increasing the automation level of formal algorithm verification.

Supporting information

zip

Zip compressed file https://doi.org/10.1107/S1600576722003107/jl5034sup1.zip
Machine-readable sources of the Isabelle/HOL proof of the correctness of the optimized and initial versions of the simple space-group-builder (core) algorithm SimpleBuilderInitial.

zip

Zip compressed file https://doi.org/10.1107/S1600576722003107/jl5034sup2.zip
The code used to generate Table 1 and to test implementations of both the initial and optimized algorithms.


Follow J. Appl. Cryst.
Sign up for e-alerts
Follow J. Appl. Cryst. on Twitter
Follow us on facebook
Sign up for RSS feeds