Skip to content

Commit

Permalink
clarify that full-functional correctness is not the specific point of…
Browse files Browse the repository at this point in the history
… this challenge, and that it suffices to focus on the transmutation-related safety invariants.
  • Loading branch information
pnkfelix committed Jun 11, 2024
1 parent fc7bcf0 commit 929dd4a
Showing 1 changed file with 2 additions and 0 deletions.
2 changes: 2 additions & 0 deletions doc/src/core-transmutation.md
Original file line number Diff line number Diff line change
Expand Up @@ -76,6 +76,8 @@ A new entry to the specification book is created explaining the relevant pattern

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.

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.


| Function | Location |
|-----------------------|-------------------|
Expand Down

0 comments on commit 929dd4a

Please sign in to comment.