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.

PropertyValue
dbpprop:abstract
  • 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.
dbpprop:designer
dbpprop:developer
dbpprop:implementations
  • an implementation is in the frama-c platform.
dbpprop:influencedBy
dbpprop:latestReleaseDate
  • December 2008
dbpprop:latestReleaseVersion
  • 2008-01-01 00:00:00 (xsd:date)
dbpprop:name
  • ANSI/ISO C Specification Language
dbpprop:paradigm
dbpprop:typing
dbpprop:wikiPageUsesTemplate
dbpprop:year
  • 2008 (xsd:integer)
rdfs:comment
  • 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.
rdfs:label
  • ANSI/ISO C Specification Language
skos:subject
foaf:page