Loading...
Please wait, while we are loading the content...
Similar Documents
Static contract checking via first-order logic.
| Content Provider | CiteSeerX |
|---|---|
| Author | Collins, Nathan |
| Abstract | Abstract. We enrich the static semantics of Haskell in order to give stronger static guarantees about the input/output behavior of programs. Our ap-proach has two parts: a contract system for Haskell, and a novel strategy for statically checking that a term satisfies a contract. The contract system includes refinement types, which refine Haskell types by arbitrary Boolean-valued Haskell expressions, and a “crash free ” pred-icate, which is true of expressions that can’t cause a run-time exception in any “safe ” context. Our novel contract-checking strategy is to translate a contract-annotated source program into a theorem in first-order logic, and then invoke an automatic theorem prover to prove (or refute) the theorem. 1 |
| File Format | |
| Access Restriction | Open |
| Subject Keyword | First-order Logic Static Contract Checking Contract System Automatic Theorem Prover Run-time Exception Safe Context Crash Free Pred-icate Novel Contract-checking Strategy Static Semantics Input Output Behavior Static Guarantee Contract-annotated Source Program Refinement Type Haskell Type Novel Strategy Arbitrary Boolean-valued Haskell Expression |
| Content Type | Text |
| Resource Type | Article |
