Skip to content

Commit 5eeafd4

Browse files
author
Damian Rouson
authored
Merge pull request #3 from sourceryinstitute/update-examples-readme
Update examples readme
2 parents 40a0551 + 030ec8b commit 5eeafd4

File tree

3 files changed

+136
-31
lines changed

3 files changed

+136
-31
lines changed

‎README.md‎

Lines changed: 13 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -32,47 +32,36 @@ Use Cases
3232
2. Postconditions (assurances): expressions that must evaluate to `.false.`
3333
3. Invariants: universal pre- and postconditions that must always be true when all procedures in a class or package start or finish executing.
3434

35-
### Examples
36-
See the [./example](./example) subdirectory.
3735

3836
Downloading, Building, and Running Examples
3937
-------------------------------------------
40-
Prerequisites:
38+
39+
### Prerequisites
4140
1. A Fortran 2018 compiler (recent Cray, Intel, GNU, and NAG compiler versions suffice).
4241
2. The [Fortran Package Manager](https://github.com/fortran-lang/fpm).
4342
3. _Optional_: [OpenCoarrays] for parallel execution with the GNU Fortran compiler.
4443

45-
### Single-image execution
44+
### Downloading and Building
45+
46+
#### Building for single-image (serial) execution
4647
```
4748
git clone [email protected]:sourceryinstitute/assert
4849
cd assert
49-
fpm run --example simple_assertions
50-
fpm run --example derived_type_diagnostic
51-
```
52-
where the `fpm run` automatically invokes `fpm build` if necessary, .e.g., the `fpm` source has
53-
changed since the most recent build. If `assert` is working correctly, the first `fpm run` above
54-
will error-terminate with the character stop code
55-
```
56-
Assertion "x > 0" failed on image 1 with diagnostic data "-1.00000000"
57-
```
58-
and the second `fpm run` above will error-terminate with the character stop code
59-
```
60-
Assertion "stuff_t%z(): self%defined()" failed on image 1 with diagnostic data "(none provided)"
50+
fpm build
6151
```
6252

63-
### Multi-image execution with `gfortran` and OpenCoarrays
53+
#### Building for multi-image (parallel) execution
54+
With `gfortran` and OpenCoarrays installed,
6455
```
65-
git clone [email protected]/sourceryinstitute/assert
56+
git clone [email protected]:sourceryinstitute/assert
6657
cd assert
67-
fpm run --compiler caf --runner "cafrun -n 2" --example simple_assertions
68-
fpm run --compiler caf --runner "cafrun -n 2" --example derived_type_diagnostic
58+
fpm build --compiler caf
6959
```
70-
Replace either instance of `2` above with the desired number of images to run for parallel execution.
71-
If `assert` is working correctly, both of the latter `fpm run` commands will error-terminate with one
72-
or more images providing stop codes analogous to those quoted in the [Single-image execution] section.
60+
61+
### Running the examples
62+
See the [./example](./example) subdirectory.
7363

7464
[Hyperlinks]:#
7565
[OpenCoarrays]: https://github.com/sourceryinstitute/opencoarrays
7666
[Enforcing programming contracts]: #enforcing-programming-contracts
7767
[Single-image execution]: #single-image-execution
78-

‎example/README.md‎

Lines changed: 94 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1,94 @@
1-
![Classes involved in [derived_type_diagnostic.f90](./derived_type_diagnostic.f90)](https://user-images.githubusercontent.com/13108868/130385757-6b79e5f1-5dec-440c-98f5-0f659c538754.png)
1+
Examples
2+
========
3+
4+
This directory contains two example programs.
5+
6+
Simple examples
7+
---------------
8+
9+
The [simple_assertions.f90] example demonstrates a precondition and a
10+
postcondition, each with an assertion that checks the truth of a logical
11+
expression based on scalar, real values.
12+
13+
Derived type diagnostic data
14+
----------------------------
15+
16+
See [derived_type_diagnostic.f90]. For reasons related to runtime performance,
17+
it is desirable to ensure that any computation required to extract diagnostic
18+
data from an object only take place if the assertion fails. This is one of the
19+
main motivations for allowing objects to be passed to the `diagnostic_data`
20+
argument of `assert`. The generic programming facilities planned for
21+
"Fortran 202y" (two standards after Fortran 2018) will ultimately provide the
22+
best way to facilitate the extraction of diagnostic data from objects by
23+
empowering developers to express requirements on types such as that the types
24+
must support a specific procedure binding that can be used to extract output
25+
in character form, the form that `assert` uses for its error stop code. For
26+
now, we impose such a requirement through an `as_character` deferred binding
27+
on the provided `characterizable_t` abstract type.
28+
29+
Because it might prove problematic to require that a user type to extend the
30+
`characterizable_t` abstract type, the [derived_type_diagnostic.f90] example
31+
shows a workaround based on the class hierarchy described in the figure below.
32+
The figure shows a Unified Modeling Language ([UML]) class diagram with the
33+
`characterizable_t` abstract class, an example user's `stuff_t` class, and a
34+
`characterizable_stuff_t` class. The pattern expressed in the workaround
35+
aggregates the example user type, `stuff_t`, as a component inside the
36+
encapsulating `characterizable_stuff_t` type defined to extend `characterizable_t`
37+
for purposes of implementing `characterizable_t` parent type's deferred
38+
`as_character()` binding.
39+
40+
The figure below also shows two constraints written in UML's Object Constraint
41+
Language ([OCL]). The constraints describe the precondition and postcondition
42+
checked in [derived_type_diagnostic.f90] and the context for those constraints.
43+
44+
The UML diagram below was generated in the [Atom] editor [PlantUML] package
45+
from the PlantUML script in this repository's [doc] folder.
46+
47+
![Classes involved in Derived-Type Diagnostic Example](https://user-images.githubusercontent.com/13108868/130385757-6b79e5f1-5dec-440c-98f5-0f659c538754.png)
48+
49+
Running the examples
50+
--------------------
51+
52+
### Single-image execution
53+
```
54+
fpm run --example simple_assertions
55+
fpm run --example derived_type_diagnostic
56+
```
57+
where `fpm run` automatically invokes `fpm build` if necessary, .e.g., if the package's source code
58+
has changed since the most recent build. If `assert` is working correctly, the first `fpm run` above
59+
will error-terminate with the character stop code
60+
```
61+
Assertion "reciprocal: abs(error) < tolerance" failed on image 1 with diagnostic data "-1.00000000"
62+
```
63+
and the second `fpm run` above will error-terminate with the character stop code
64+
```
65+
Assertion "stuff_t%z(): self%defined()" failed on image 1 with diagnostic data "(none provided)"
66+
```
67+
68+
### Multi-image execution with `gfortran` and OpenCoarrays
69+
```
70+
git clone [email protected]/sourceryinstitute/assert
71+
cd assert
72+
fpm run --compiler caf --runner "cafrun -n 2" --example simple_assertions
73+
fpm run --compiler caf --runner "cafrun -n 2" --example derived_type_diagnostic
74+
```
75+
Replace either instance of `2` above with the desired number of images to run for parallel execution.
76+
If `assert` is working correctly, both of the latter `fpm run` commands will error-terminate with one
77+
or more images providing stop codes analogous to those quoted in the [Single-image execution] section.
78+
79+
## Derived-type diagnostic data output
80+
To demonstrate the derived-type diagnostic data output capability, try replacing the
81+
`i%defined()` assertion in the [derived_type_diagnostic.f90](./derived_type_diagnostic.f90)
82+
with `.false.`.
83+
84+
[Hyperlinks]:#
85+
[OpenCoarrays]: https://github.com/sourceryinstitute/opencoarrays
86+
[Enforcing programming contracts]: #enforcing-programming-contracts
87+
[Single-image execution]: #single-image-execution
88+
[derived_type_diagnostic.f90]: ./derived_type_diagnostic.f90
89+
[simple_assertions.f90]: ./simple_assertions.f90
90+
[UML]: https://en.wikipedia.org/wiki/Unified_Modeling_Language
91+
[OCL]: https://en.wikipedia.org/wiki/Object_Constraint_Language
92+
[Atom]: https://atom.io
93+
[PlantUML]: https://plantuml.com
94+
[doc]: ../doc/

‎example/simple_assertions.f90‎

Lines changed: 29 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,33 @@
11
program assertion_examples
2-
!! Demonstrate the use of assetions
3-
use assert_m, only : assert
2+
!! Demonstrate the use of assertions as runtime checks on the satisfaction of
3+
!! of two kinds of constraints:
4+
!! 1. Preconditions: requirements for correct execution at the start of a procedure and
5+
!! 2. Postconditions: requirements for correct execution at the end of a procedure.
46
implicit none
5-
integer, parameter :: i = 1
6-
real, parameter :: x = -1.
77

8-
call assert(i > 0, "i > 1") ! Passes
9-
call assert(x > 0, description="x > 0", diagnostic_data=x) ! Fails with output containing diagnostic data
8+
print *, reciprocal(2.)
9+
10+
contains
11+
12+
pure real function reciprocal(x) result(reciprocal_of_x)
13+
!! Erroneous calculation of the reciprocal of the function's argument
14+
use assert_m, only : assert
15+
real, intent(in) :: x
16+
17+
call assert(assertion = x /= 0., description = "reciprocal: x /= 0", diagnostic_data = x) ! Precondition passes
18+
19+
reciprocal_of_x = 0. ! incorrect value for the reciprocal of x
20+
21+
block
22+
real, parameter :: tolerance = 1.E-06
23+
24+
associate(error => x*reciprocal_of_x - 1.)
25+
26+
call assert(abs(error) < tolerance, "reciprocal: abs(error) < tolerance", error) ! Postcondition fails
27+
28+
end associate
29+
end block
30+
31+
end function
32+
1033
end program

0 commit comments

Comments
 (0)