@@ -23,8 +23,8 @@ between 0 and 255. The functional correctness is therefore preserved.
With respect to functional correctness, we define the post condition:
memory fragment sa contains some value a, memory fragment sb contains some value b,
memory fragment sc contains some value equal to f(a,b). This fixes your result.
Adding length constraints on those values further complicate the post condition.
Adding length constraints on those values further complicate the post condition but are necessary.
With this postcondition at hand, the Coq proof system with VST will prevent you to prove the function correctness if you do not have the correct and necessary preconditions. It is not possible to miss a critical precondition, this is provided by the semantic of the VST. As a result, we can say that our preconditions are minimal.
With those postconditions at hand, the Coq proof system with VST will prevent you to prove the function correctness if you do not have the necessary preconditions. It is not possible to miss a critical precondition, this is provided by the semantic of the VST. As a result, we can say that our preconditions are minimal.
Additionally, Adding unnecessary precondition violates Occam's razor principle and risks adding inconsistencies and contradictions.
Additionally, Adding unnecessary precondition violates Occam's razor principle and risks adding inconsistencies and contradictions, which would render our proof useless.
