Authors

Carlos López Pombo, Sam Owre, and Natarajan Shankar

Abstract

Ag is a specification language presented as a syntactic sugaring of the First-Order Dynamic Logic of Fork Algebras. This language is particularly attractive due to its expressive power, easy-to-understand semantics, and the existence of a complete deductive system. We will briefly present the language together with a complete deductive calculus and some theoretical results about its expressive power. We then show how the higher-order logic theorem prover PVS can be used to build a semantic framework for reasoning about specifications written in Ag by encoding the semantics within this powerful general-purpose tool. We then illustrate how this semantic embedding can be used by means of a case study of a cache system specification.

PDF PS

BibTeX Entry

@techreport{Ag-in-PVS,
	AUTHOR = {Carlos L\'{o}pez Pombo and Sam Owre and Natarajan Shankar},
	INSTITUTION = csl,
	TITLE = {A Semantic Embedding of the {Ag} Dynamic Logic in {PVS}},
	MONTH = oct,
	YEAR = 2004,
	NUMBER = {SRI-CSL-02-04},
	ADDRESS = {Menlo Park, CA},
	NOTE = {Available at
	        \url{http://pvs.csl.sri.com/papers/AgExample/}}
}