Back to Search
Start Over
The bedrock structured programming system
- Source :
- ICFP, MIT web domain
- Publication Year :
- 2013
- Publisher :
- Association for Computing Machinery (ACM), 2013.
-
Abstract
- We report on the design and implementation of an extensible programming language and its intrinsic support for formal verification. Our language is targeted at low-level programming of infrastructure like operating systems and runtime systems. It is based on a cross-platform core combining characteristics of assembly languages and compiler intermediate languages. From this foundation, we take literally the saying that C is a "macro assembly language": we introduce an expressive notion of certified low-level macros, sufficient to build up the usual features of C and beyond as macros with no special support in the core. Furthermore, our macros have integrated support for strongest postcondition calculation and verification condition generation, so that we can provide a high-productivity formal verification environment within Coq for programs composed from any combination of macros. Our macro interface is expressive enough to support features that low-level programs usually only access through external tools with no formal guarantees, such as declarative parsing or SQL-inspired querying. The abstraction level of these macros only imposes a compile-time cost, via the execution of functional Coq programs that compute programs in our intermediate language; but the run-time cost is not substantially greater than for more conventional C code. We describe our experiences constructing a full C-like language stack using macros, with some experiments on the verifiability and performance of individual programs running on that stack.<br />United States. Defense Advanced Research Projects Agency (Agreement FA8750-12-2-0293))
- Subjects :
- Computer science
Hoare logic
computer.software_genre
Extensibility
Extensible programming
Third-generation programming language
Macro
Fifth-generation programming language
Formal verification
Obstack
computer.programming_language
Intermediate language
Functional programming
geography
geography.geographical_feature_category
Assembly language
Programming language
Bedrock
Inline expansion
Structured programming
Metaprogramming
Computer Graphics and Computer-Aided Design
Postcondition
Compiler
Low-level programming language
computer
Software
Subjects
Details
- ISSN :
- 15581160 and 03621340
- Volume :
- 48
- Database :
- OpenAIRE
- Journal :
- ACM SIGPLAN Notices
- Accession number :
- edsair.doi.dedup.....528a2d4fa33003abee08ccb711b54b5f