Skip to content

Commit 929dd4a

Browse files
committed
clarify that full-functional correctness is not the specific point of this challenge, and that it suffices to focus on the transmutation-related safety invariants.
1 parent fc7bcf0 commit 929dd4a

File tree

1 file changed

+2
-0
lines changed

1 file changed

+2
-0
lines changed

doc/src/core-transmutation.md

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -76,6 +76,8 @@ A new entry to the specification book is created explaining the relevant pattern
7676

7777
At least 35 of the following 47 intrinsics and functions (i.e. approximately 75%) have been annotated with contracts, and, for non-intrinsics, had their bodies verified.
7878

79+
For the safe functions, you do not need to provide a full-functional correctness specificatipn; it will suffice to add pre- and post-conditions (i.e. assumptions and assertions) around the relevant part of the code that calls the transmutation-related unsafe function or intrinsic.
80+
7981

8082
| Function | Location |
8183
|-----------------------|-------------------|

0 commit comments

Comments
 (0)