Loading...
Please wait, while we are loading the content...
Similar Documents
Language-agnostic Contract specification and checking with CodeContracts and Clousot
| Content Provider | Semantic Scholar |
|---|---|
| Author | Aspinall, David Chong, Stephen Coglio, Alessandro Crégut, Pierre Genaim, Samir Hansen, René Rydhof Jacobs, Bart |
| Copyright Year | 2010 |
| Abstract | CodeContracts allow specifying contracts (preconditions, postconditions and object invariants) in a language agnostic form. Contracts are expressed as calls to static methods of the homonymous class included in .NET 4.0. They are serialized and persisted as bytecode, achieving language agnosticism. Runtime checking is performed via bytecode rewriting. The static checker, Clousot, directly analyzes the bytecode to validate the user-provided contracts as well as the absence of common runtime errors. Clousot is based on abstract interpretation, and as such it can presents a higher level of automatism (e.g. for the inference of loop invariants, or postconditions) with respect to similar tools. Also, it scales up to large codebases thanks to the use of new numerical abstract domains and adaptive techniques (which I will sketch in the talk). |
| File Format | PDF HTM / HTML |
| Alternate Webpage(s) | http://bytecode2010.inria.fr/pproc.pdf |
| Alternate Webpage(s) | http://www.researchgate.net/profile/Premek_Brada/publication/220367589_Reconstruction_of_Type_Information_from_Java_Bytecode_for_Component_Compatibility/links/0f31752e53c2eb55ef000000.pdf |
| Alternate Webpage(s) | https://www.researchgate.net/profile/Premek_Brada/publication/220367589_Reconstruction_of_Type_Information_from_Java_Bytecode_for_Component_Compatibility/links/0f31752e53c2eb55ef000000.pdf |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |