Providing mechanical support for program development in a weakest precondition calculus
Date
1993-04
Authors
Ackerman, Charlotte Christene
Journal Title
Journal ISSN
Volume Title
Publisher
Stellenbosch : Stellenbosch University
Abstract
ENGLISH ABSTRACT: Formal methods aim to apply the rigour of mathematical logic to the problem ofguaranteeing that the behaviour of (critical) software conforms to predetermined requirements. The application of formal methods during program construction centers around a formal specification of the required behaviour of the program. A development attempt is successful if the resulting program can be formally proven to conform to its specification. For any substantial program, this entails a great deal of effort. Thus, some research efforts have been directed at providing mechanical support for the application of formal methods to software development. E.W. Dijkstra's calculus of weakest precondition predicate transformers [39,38] represents one of the first attempts to use program correctness requirements to guide program development in a formal manner.
AFRIKAANSE OPSOMMING: Formele metodes poog om die strengheid van wiskundige logika te gebruik om te waarborg dat die gedrag van (kritiese) programmatuur voldoen aan gegewe vereistes. Die toepassing van formele metodes tydens programontwikkeling sentreer rondom a formele spesifikasie van die verlangde programgedrag. 'n Ontwikkelingspoging is suksesvol as daar formee1 bewys kan word dat die resulterende program aan sy spesifikasie voldoen. Vir enige substansiële program, verteenwoordig dit ‘n aansienlike hoeveelheid werk. Verskeie navorsinspoging is gerig op die daarstelling van meganiese ondersteuning vir die gebruik van formele metodes tydens ontwikkeling van sagteware. E. W. Dijkstra se calculus van swakste voorkondisie (“weakest precondition”) predikaattransformators [39,38] is een van die eerste pogings om vereistes vir programkorrektheid op ‘n formele en konstruktiewe wyse tydens programontwikkeling te gebruik.
AFRIKAANSE OPSOMMING: Formele metodes poog om die strengheid van wiskundige logika te gebruik om te waarborg dat die gedrag van (kritiese) programmatuur voldoen aan gegewe vereistes. Die toepassing van formele metodes tydens programontwikkeling sentreer rondom a formele spesifikasie van die verlangde programgedrag. 'n Ontwikkelingspoging is suksesvol as daar formee1 bewys kan word dat die resulterende program aan sy spesifikasie voldoen. Vir enige substansiële program, verteenwoordig dit ‘n aansienlike hoeveelheid werk. Verskeie navorsinspoging is gerig op die daarstelling van meganiese ondersteuning vir die gebruik van formele metodes tydens ontwikkeling van sagteware. E. W. Dijkstra se calculus van swakste voorkondisie (“weakest precondition”) predikaattransformators [39,38] is een van die eerste pogings om vereistes vir programkorrektheid op ‘n formele en konstruktiewe wyse tydens programontwikkeling te gebruik.
Description
Thesis (MSc)--Stellenbosch University, 1993.
Keywords
Mathematical logic, Calculus -- Computer programs, Theses -- Computer science, Dissertations -- Computer science, Computer software -- Development