摘要: The goal of this work is to provide a clean formal framework to support the development of programs integrating modules of di erent styles (eg, Horn clauses modules, equational modules, functional modules, constraints based modules,:::). Di erent modules could be developed each in its own style bene ting of all methods and tools available for the particular style. The framework presents then a uniform and high-level view allowing to make reasoning about those modules (analysis, optimization, proofs), and to integrate them adequately in a realistic program.The idea is to de ne a language whose syntax and semantics are su ciently general so as the di erent modules of the di erent styles can be considered as particular (possibly incomplete) implementations of that language. The language can be considered as an intermediate description between a speci cation and a program. The key ideas are the following:
参考文章(0)