... | ... | @@ -18,6 +18,8 @@ In Compcert some datatypes are defined my mutual induction ([expr] and [statemen |
|
|
|
|
|
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.
|
|
|
|
|
|
(To be continued)
|
|
|
|
|
|
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 ?
|
|
|
|
|
|
|
... | ... | |