Skip to content

Commit efb0712

Browse files
committed
Minor correction to the original text of design_by_contract.txt.
In reviewing the paper prior to submitting a pull request I realized that I had misspelled .EQV. as .EQUIV. and that I had forgotten to mention ASSERT at one point where I discussed REQUIRES and ENSURES. [ticket: j3-fortran#70]
1 parent fcaee84 commit efb0712

File tree

1 file changed

+22
-18
lines changed

1 file changed

+22
-18
lines changed

proposals/assert/design_by_contract.txt

+22-18
Original file line numberDiff line numberDiff line change
@@ -5,8 +5,10 @@ Date: August 1, 2020
55
#Reference: 04-142.txt, 04-143.txt, 04-144.txt, 04-212.txt,
66
04-219.txt, 04-376.txt, 04-414.txt
77

8+
89
Proposal for Fortran Standard: 202y (NOT 202x)
910

11+
1012
1. Introduction
1113

1214
This paper contains a proposal to allow programmers to use "Design by
@@ -40,11 +42,11 @@ tests can be active during testing, and inactive on deployment.
4042

4143
DbC can be met with a minimum of one new statement, for testing
4244
anywhere in the code body, say ASSERT, but ideally there would be
43-
three new statements: one to be used at the start of the procedure to
44-
test pre-conditions, say REQUIRES, and one to be used immediately
45-
before the procedure's return to test post-conditions, say
46-
ENSURES. All three statements would be simple in form and have simple
47-
semantics.
45+
three new statements: one the equivalent of ASSERT, one to be used at
46+
the start of the procedure to test pre-conditions, say REQUIRES, and
47+
one to be used immediately before the procedure's return to test
48+
post-conditions, say ENSURES. All three statements would be simple in
49+
form and have simple semantics.
4850

4951

5052
2. Problem
@@ -66,6 +68,7 @@ with appropriate pre-processor flags, but does require a dependence
6668
on a preprocessor. None document for the user the pre and post
6769
conditions the user can expect for properly working code.
6870

71+
6972
3. Use cases
7073

7174
A simple function that requires non-negative integer arguments.
@@ -104,7 +107,7 @@ other optional argument is present.
104107

105108
SUBROUTINE OPTIONALS( A, B )
106109
TYPE(EXAMPLE), OPTIONAL, INTENT(IN) :: A, B
107-
REQUIRES( PRESENT(A) .EQUIV. PRESENT(B) )
110+
REQUIRES( PRESENT(A) .EQV. PRESENT(B) )
108111
...
109112
RETURN
110113
END SUBROUTINE OPTIONALS
@@ -126,7 +129,7 @@ A test of a problematic procedure call
126129

127130
The term design by contract as applied to programming languages has
128131
its origins in the language Eiffel.[4,5] Since then, in addition to
129-
C++ it has been adopted by Ada,[6] D[7] and Fortress. The C standard
132+
C++ it has been adopted by Ada,[6] D,[7] and Fortress. The C standard
130133
library comes with the assert macro so C can be said to partially
131134
support DbC. To our knowledge no Fortran compiler has implemented
132135
anything to support DbC. Many users implement their own equivalent of
@@ -137,17 +140,17 @@ capabilities.
137140
5. Specification
138141

139142
All three statements will have similar behavior. All three will take
140-
as their sole argument a scalar logical expression, that if
141-
.TRUE. does nothing, and if .FALSE. writes output to the ERROR_UNIT of
142-
ISO_FORTRAN_ENV and stops as if ERROR STOP was invoked. The writes
143-
will all indicate the location of the executed statement: either the
144-
procedure name with the name of the enclosing module, or the name of
145-
the file including the statement and the line number of the statement,
146-
or both. All three will write out the text of the logical expression
147-
that failed, with a prefix. The prefix will differ between the three
148-
statements. Example prefixes for the REQUIRES statement is
149-
"PRE-CONDITION FAILED: ", for the ASSERTS statement is "ASSERTION
150-
FAILED: ". and for the ENSURES statement is "POST-CONDITION
143+
as their arguments a list of scalar logical expressions, that if all
144+
.TRUE. does nothing, and if one is .FALSE. writes output to the
145+
ERROR_UNIT of ISO_FORTRAN_ENV and stops as if ERROR STOP was
146+
invoked. The writes will all indicate the location of the executed
147+
statement: either the procedure name with the name of the enclosing
148+
module, or the name of the file including the statement and the line
149+
number of the statement, or both. All three will write out the text of
150+
the logical expression that failed, with a prefix. The prefix will
151+
differ between the three statements. Example prefixes for the REQUIRES
152+
statement is "PRE-CONDITION FAILED: ", for the ASSERTS statement is
153+
"ASSERTION FAILED: ". and for the ENSURES statement is "POST-CONDITION
151154
FAILED: ".
152155

153156
The semantics of all three statements are similar. They all should
@@ -162,6 +165,7 @@ processing. They should have restrictions similar to those of ERROR
162165
STOP, being allowed in PURE procedures, but not in ELEMENTAL
163166
procedures.
164167

168+
165169
4. Syntactic options
166170

167171
The syntax for the statements depend on whether they should be

0 commit comments

Comments
 (0)