Annotations in formal specifications and proofs (Q1334901)
From MaRDI portal
 | This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use this page instead for the normal view: Annotations in formal specifications and proofs |
scientific article; zbMATH DE number 644674
| Language | Label | Description | Also known as |
|---|---|---|---|
| English | Annotations in formal specifications and proofs |
scientific article; zbMATH DE number 644674 |
Statements
Annotations in formal specifications and proofs (English)
0 references
26 September 1994
0 references
In order to exploit the connection between the formal and the informal aspects of modeling, the author proposes a system of annotations that can be used to incorporate semantic information concerning the domain being reasoned about into a formal proof environment. Annotations will serve as comments, labels, or proof directives. An implementation in the HOL proof system is presented.
0 references
formal specification
0 references
verification
0 references
theorem proving
0 references
modeling
0 references
