Name
Abstract | ||
|---|---|---|
We propose a definition of hierarchical heterogeneous formal specifications, where each module is specified according to its own homogeneous logic. We focus on the specification structure which we represent by a term in order to take benefit of classical knowledge on terms. For example, substitutions solve implementation sharing of modules. Then, we show how proof mechanisms can be expressed inside our framework. Our proof system involves both the homogeneous inference relations associated to the logics of modules and property inheritance relations associated to the structuring primitives. Heterogeneous primitives allow to move from one logic to another. We sketch out the specification of a travel agency given according to our particular framework of structured specifications. We demonstrate on this specification how a heterogeneous proof can be handled. |
Year | DOI | Venue |
|---|---|---|
1998 | 10.1007/3-540-48483-3_8 | WADT |
Keywords | Field | DocType |
heterogeneous proof,hierarchical heterogeneous formal specification,homogeneous inference relation,own homogeneous logic,structured specification,heterogeneous primitive,proof system,hierarchical heterogeneous specifications,particular framework,specification structure,proof mechanism,logical framework,proof theory | Algebraic specification,Inference,Computer science,Algorithm,Proof theory,Formal specification,Theoretical computer science,Structuring,Modularity,Logical framework,Sketch | Conference |
Volume | ISSN | ISBN |
1589 | 0302-9743 | 3-540-66246-4 |
Citations | PageRank | References |
2 | 0.42 | 18 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Sophie Coudert | 1 | 19 | 3.14 |
| Gilles Bernot | 2 | 480 | 44.25 |
| Pascale Le Gall | 3 | 287 | 32.95 |