... | ... | @@ -16,13 +16,16 @@ In Compcert some datatypes are defined my mutual induction ([expr] and [statemen |
|
|
|
|
|
(To be continued)
|
|
|
|
|
|
## Patched semantics
|
|
|
## Using 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.
|
|
|
|
|
|
(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 ?
|
|
|
## Composing Patched semantics
|
|
|
|
|
|
When we have two independent patched semantics, how to build a new semantics which is the composition of the two first ones ? In particular, can we do it without using copies of proof scripts but by reusing existing proofs ?
|
|
|
|
|
|
|
|
|
(To be continued)
|
|
|
|