... | ... | @@ -14,4 +14,11 @@ In Compcert some datatypes are defined my mutual induction ([expr] and [statemen |
|
|
|
|
|
(To be continued)
|
|
|
|
|
|
## Patched semantics |
|
|
\ No newline at end of file |
|
|
## Patched semantics
|
|
|
|
|
|
To ease some proofs we can develop a variant of the semantics of C programs defined in cfrontend/Csem and prove that this variant is equivalent to the original semantics.
|
|
|
|
|
|
Now, when we have developed two independent variants, and proved their correctness, how to build a new variant which is the composition of the two atomic variants ? In particular, can we do it without using copies of proof scripts but by reusing existing proofs ?
|
|
|
|
|
|
|
|
|
|