Name: Annotations in formal specifications and proofs
Creator: Saraswati Kalvala
Keywords: formal specification, Specification and verification (program logics, model checking, etc.), theorem proving, 0202 electrical engineering, electronic engineering, information engineering, modeling, 02 engineering and technology, 0101 mathematics, verification, 01 natural sciences, Theorem proving (deduction, resolution, etc.)

descriptionPublicationkeyboard_double_arrow_right Article 01 Jul 1994 English Publisher:Springer Science and Business Media LLCJournal:Formal Methods in System Design, volume 5, pages 119-144 (issn: 0925-9856, eissn: 1572-8102,

Authors: Saraswati Kalvala;

doi: 10.1007/bf01384236

Annotations in formal specifications and proofs

- Summary
- Subjects
- Metrics

Abstract

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.

Related Organizations

University of Cambridge
United Kingdom

Keywords

formal specification, Specification and verification (program logics, model checking, etc.), theorem proving, modeling, verification, Theorem proving (deduction, resolution, etc.)

Impact byBIP!

	citations This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).	4
	popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.	Average
	influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).	Average
	impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.	Average

Found an issue? Give us feedback

Average

Fields of Science (4) View all

Fields of Science

Upload OA version

Are you the author of this publication? Upload your Open Access version to Zenodo!

It’s fast and easy, just two clicks!

uploadUpload now