### Skapa referens, olika format (klipp och klistra)

**Harvard**

Szasz, N. (1997) *A Theory of Specifications Programs and Proofs*. Göteborg : Chalmers University of Technology (Doktorsavhandlingar vid Chalmers tekniska högskola. Ny serie, nr: 1302).

** BibTeX **

@book{

Szasz1997,

author={Szasz, Nora},

title={A Theory of Specifications Programs and Proofs},

isbn={91-7197-510-1},

abstract={Using Martin-Löf's set theory as a programming logic one identifies specifications with sets and propositions and, correspondingly, programs with elements of sets and with proofs. Then, programs happen to contain something else than just what is needed to perform computations. In this work we investigate a theory in which the notion of program as a method of computation is singled out. As a first step towards a theory of specifications, we separate the notions of data type and proposition and define a calculus for program verification, where programs can be written and then proved correct. Based on this calculus, a theory of specifications is built up. A specification of a problem consists of a pair: a data type for a program and a predicate on the program. Such a specification is implemented by constructing a program of the given data type and proving that the predicate holds for that program. We are interested in a calculus of program derivation, i.e. a calculus with rules that allow the simultaneous construction of the components of implementations, rather than the separate construction of programs and proofs. The theory of specifications is built up in such a way that the program extraction process is immediate.},

publisher={Institutionen för datavetenskap, Chalmers tekniska högskola,},

place={Göteborg},

year={1997},

series={Doktorsavhandlingar vid Chalmers tekniska högskola. Ny serie, no: 1302},

}

** RefWorks **

RT Dissertation/Thesis

SR Print

ID 1272

A1 Szasz, Nora

T1 A Theory of Specifications Programs and Proofs

YR 1997

SN 91-7197-510-1

AB Using Martin-Löf's set theory as a programming logic one identifies specifications with sets and propositions and, correspondingly, programs with elements of sets and with proofs. Then, programs happen to contain something else than just what is needed to perform computations. In this work we investigate a theory in which the notion of program as a method of computation is singled out. As a first step towards a theory of specifications, we separate the notions of data type and proposition and define a calculus for program verification, where programs can be written and then proved correct. Based on this calculus, a theory of specifications is built up. A specification of a problem consists of a pair: a data type for a program and a predicate on the program. Such a specification is implemented by constructing a program of the given data type and proving that the predicate holds for that program. We are interested in a calculus of program derivation, i.e. a calculus with rules that allow the simultaneous construction of the components of implementations, rather than the separate construction of programs and proofs. The theory of specifications is built up in such a way that the program extraction process is immediate.

PB Institutionen för datavetenskap, Chalmers tekniska högskola,

T3 Doktorsavhandlingar vid Chalmers tekniska högskola. Ny serie, no: 1302

LA eng

OL 30