Abstract | ||
---|---|---|
We believe that big software systems could be more easily formally specified if several specification approaches were allowed within a single system specification. We propose a notion of heterogeneous framework where the specifier can choose a dedicated specification framework for each specification module. We show how the resulting heterogeneous modular specifications can get semantics, and how modular proofs can still be performed on these specifications. Our contribution is mainly focussed on a sort of interoperability between heterogeneous specification modules and we retrieve, as much as possible, classical notions of "meta-formalisms," modularity for structured specifications, or inference systems, as they are well known in the algebraic specification community. With this respect, our work can be regarded as an attempt to unify frameworks, by accepting and formalizing heterogeneity. |
Year | DOI | Venue |
---|---|---|
1996 | 10.1007/BFb0014333 | AMAST |
Keywords | Field | DocType |
algebraic specifications,formal specifications,in- ference systems,heterogeneous specifications,modularity,logical frameworks,theorem proving.,towards heterogeneous formal specification,software systems,formal specification,logical framework,theorem proving | Specification language,Algebraic specification,Z notation,Programming language,Computer science,Formal specification,Theoretical computer science,Language Of Temporal Ordering Specification,Formal methods,Software requirements specification,System requirements specification | Conference |
ISBN | Citations | PageRank |
3-540-61463-X | 4 | 0.49 |
References | Authors | |
16 | 3 |
Name | Order | Citations | PageRank |
---|---|---|---|
Gilles Bernot | 1 | 480 | 44.25 |
Sophie Coudert | 2 | 19 | 3.14 |
Pascale Le Gall | 3 | 287 | 32.95 |