... | ... | @@ -2,10 +2,16 @@ This page describes some interesting points that have been encountered during th |
|
|
|
|
|
## Concepts of behavior preservation
|
|
|
|
|
|
Compilation steps can forget some behaviors or refine undefined behaviors. When refactoring, is possible, we want to preserve exactly the set of possible behaviors and not to refine undefined behaviors.
|
|
|
Compilation steps can forget some behaviors or refine undefined behaviors. When refactoring a program, however, if possible, we want to preserve exactly the set of possible behaviors and not to refine undefined behaviors.
|
|
|
|
|
|
(To be continued)
|
|
|
|
|
|
## Mutual induction
|
|
|
|
|
|
(Proof engineering in Coq)
|
|
|
|
|
|
In Compcert some datatypes are defined my mutual induction ([expr] and [statement] in particular). Also in RefacCert some constructions are also defined by mutual recursion or induction. We have met some cases where Coq consumes too many memory or too many time to deal with proofs on those constructions. We discuss the workarounds we have used in these cases.
|
|
|
|
|
|
(To be continued)
|
|
|
|
|
|
## Patched semantics |
|
|
\ No newline at end of file |