Abstract | ||
---|---|---|
It is widely recognized that abstraction and modularization are indispensable for specification of real-world programs. In source-code level program specification and verification, model fields are a common means for those goals. However, it remains a challenge to provide a well-founded formal semantics for the general case in which the abstraction relation defining a model field is non-functional. In this paper, we discuss and compare several possibilities for defining model field semantics, and we give a complete formal semantics for the general case. Our analysis and the proposed semantics is based on a generalization of Hilbert's ε terms. |
Year | DOI | Venue |
---|---|---|
2012 | 10.1007/978-3-642-33347-7_2 | KI |
Keywords | Field | DocType |
model field,proposed semantics,source-code level program specification,defining model field semantics,real-world program,common mean,abstraction relation,general case,annotation-based specification,well-founded formal semantics,complete formal semantics | Formal semantics (linguistics),Operational semantics,Programming language,Computational semantics,Computer science,Denotational semantics,Action semantics,Theoretical computer science,Formal specification,Well-founded semantics,Formal verification | Conference |
Citations | PageRank | References |
0 | 0.34 | 8 |
Authors | ||
2 |
Name | Order | Citations | PageRank |
---|---|---|---|
Bernhard Beckert | 1 | 862 | 86.50 |
Daniel Bruns | 2 | 76 | 4.96 |