Skip to content

Commit 508df43

Browse files
committed
Correct contract documentation about loops
1 parent 228b9dd commit 508df43

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/goto-instrument/contracts/doc/user/contracts-loops.md

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ Back to @ref contracts-user
44

55
@tableofcontents
66

7-
CBMC offers support for loop contracts, which includes three basic clauses:
7+
CBMC offers support for loop contracts, which includes four basic clauses:
88
- an _invariant_ clause for establishing safety properties,
99
- a _decreases_ clause for establishing termination,
1010
- an _assigns_ clause for declaring the memory locations assignable by the loop,

0 commit comments

Comments
 (0)