词条 | ANSI/ISO C Specification Language |
释义 |
}}{{Infobox programming language | name = ANSI/ISO C Specification Language | paradigm = declarative with few imperative features. | year = 2008 | designer = Commissariat à l'Énergie Atomique and INRIA | developer = Commissariat à l'Énergie Atomique and INRIA | latest release version = 2008 | latest release date = December 2008 | typing = static | implementations = an implementation is in the Frama-C platform. | influenced_by = JML }} The ANSI/ISO C Specification Language (ACSL) is a specification language for C programs, using Hoare style pre- and postconditions and invariants, that follows the design by contract paradigm. Specifications are written as C annotation comments to the C program, which hence can be compiled with any C compiler. The current verification tool for ACSL is Frama-C. OverviewIn 1983, the American National Standards Institute (ANSI) commissioned a committee, X3J11, to standardize the C language. The first standard for C was published by ANSI. Although this document was subsequently adopted by International Organization for Standardization (ISO) and subsequent revisions published by ISO have been adopted by ANSI, the name ANSI C continues to be used. ACSL is a Behavioral Interface Specification Language (BISL). It aims at specifying behavioral properties of C source code. The main inspiration for this language comes from the specification language of the Caduceus tool for deductive verification of behavioral properties of C programs. The specification language of Caduceus is itself inspired from JML which aims at similar goals for Java source code. One difference with JML, is that ACSL aims at static verification and deductive verification whereas JML aims both at runtime assertion checking and static verification using for instance the ESC/Java tool. SyntaxLet us consider the following example for the prototype of a function named The contract is given by the comment which starts with
Tool supportMost of the features of ACSL are supported by Frama-C. References
External linksThe complete ACSL specification is available from the download page of Frama-C. {{DEFAULTSORT:ANSI ISO C Specification Language}} 2 : Specification languages|C (programming language) |
随便看 |
|
开放百科全书收录14589846条英语、德语、日语等多语种百科知识,基本涵盖了大多数领域的百科知识,是一部内容自由、开放的电子版国际百科全书。