CamFort is a multi-feature tool for improving the quality of Fortran code. Its features are primarily aimed at programming patterns found in numerical modelling code e.g., in computational science.
CamFort is free and open-source. It currently supports Fortran 66, 77, 90, and 95 language standards. Support for Fortran 2003, and 2008 is in progress.
- 18th May 2018 -
v0.905 of CamFort has been released
. The main changes are:
- Extended support for Fortran 95 & legacy extensions;
- Improved units-of-measure checking (performance & functionality)
- Prototype for Hoare logic style verification assertions back by SMT solving
- October 2017 - Our paper Verifying Spatial Properties of Array Computations has been accepted at the ACM OOPSLA 2017 conference. Dominic will present the paper in Vancouver on 26th of October.
- 26th July 2017 -
v0.904 of CamFort has been released
. The main changes are:
- Better protection against dependencies breaking builds;
- Significantly reduced build time;
- Better command line interface;
- Improved error messages;
- Bug fixes to stencil specifications
- 24-26th July 2017 - We are talking about CamFort at the Fortran modernization workshop at Universitat Politechnica de Catalunya, Barcelona, Spain. (details).
- 30th May 2017 -
v0.902 of CamFort has been released. The main changes are:
- Improved stencil specification support;
- Polymorphic unit signatures (see this example);
- Much faster verification times.
Specification & verification
CamFort provides lightweight verification features. Source-code annotations (comments) provide specifications of certain aspects of a program's meaning or behaviour. CamFort can then check that code conforms to these specifications. CamFort can also suggest places to insert specifications, and in some cases case infer the specifications of existing code.
Our current specification and verification features provide:
- Units-of-measure typing allows you to annotate Fortran
source code with units of variables and can automatically check
whether units are consistently used and report back where it went
wrong if they are inconsistent.
!= unit(m) :: d1, d2 != unit(s) :: t real :: d1, d2, t, v v = (d1 + d2)/t
- Array access shape allows you to describe and verify
the access patterns your code makes over arrays in order to catch
array indexing errors. Example:
do i = 1, n do j = 1, m x = a(i, j-1) + a(i, j+1) + a(i, j) y = a(i+1, j-1) + a(i+1, j+1) + a(i+1, j) != stencil forward(dim=1,depth=1) * centered(dim=2,depth=1) :: a b(i, j) = x + y end do end do
Many language features of older Fortran standards (pre Fortran 90) are known to be a ready source of programming error. CamFort provides some facilities for automatically refactoring deprecated or dangerous programming patterns, with the goal of helping to meet core quality requirements, such as maintainability. For example, our tool eliminates EQUIVALENCE and COMMON blocks. These refactorings also helps to expose any programming bugs arising from bad programming practices.
Programming languages provide an interface for developing increasingly complex models in science. However, as computer models grow more complex, it is increasingly difficult to deliver on core requirements such as verifiability, maintainability, understandability, validity, and portability.
Managing software complexity more effectively has been a focus of programming language research for many years, yet we see little adoption of new approaches in the natural sciences. Instead we see scientists continually striving to evolve their software to more complex models, or bigger data sets or novel execution architectures.
Our objectives are:
- Crossing the chasm: To show how programming language ideas such as inference of high-level programming patterns, advanced types and automatic test generation can be used to reduce the accidental complexity of real scientific code, and improve its evolution, maintainability, and verification.
- Practical adoption: To develop tools for maintaining and evolving established, long-lived code-bases. To apply these ideas without disrupting existing practices by accommodating the various incarnations of the language, and (custom) pre-processors.
- Closing the chasm: To provide a framework which makes it easier to transfer future programming language research in to practice in computational science.