Providing mechanical support for program development in a weakest precondition calculus

Simple item page
dc.contributor.advisorDe Villiers, P. J. A.
dc.contributor.authorAckerman, Charlotte Christene
dc.contributor.otherUniversity of Stellenbosch. Faculty of Science. Dept. of Mathematical Sciences
dc.date.accessioned2013-01-29T10:38:02Z
dc.date.available2013-01-29T10:38:02Z
dc.date.issued1993-04
dc.descriptionThesis (MSc)--Stellenbosch University, 1993.en_ZA
dc.description.abstractENGLISH 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.en_ZA
dc.description.abstractAFRIKAANSE 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.af_ZA
dc.format.extent202 p.
dc.identifier.urihttp://hdl.handle.net/10019.1/79317
dc.language.isoen_ZAen_ZA
dc.publisherStellenbosch : Stellenbosch Universityen_ZA
dc.rights.holderStellenbosch Universityen_ZA
dc.subjectMathematical logicen_ZA
dc.subjectCalculus -- Computer programsen_ZA
dc.subjectTheses -- Computer scienceen_ZA
dc.subjectDissertations -- Computer scienceen_ZA
dc.subjectComputer software -- Developmenten_ZA
dc.titleProviding mechanical support for program development in a weakest precondition calculusen_ZA
dc.typeThesisen_ZA
Files
Original bundle
Now showing 1 - 1 of 1
Thumbnail Image
Name:
ackerman_mechanical_1993.pdf
Size:
7.85 MB
Format:
Adobe Portable Document Format
Description:
Download
License bundle
Now showing 1 - 1 of 1
Thumbnail Image
Name:
license.txt
Size:
1.95 KB
Format:
Item-specific license agreed upon to submission
Description:
Download
Collections
Masters Degrees (Mathematical Sciences)