Full Text Available
Note: Clicking the button above will open the full text document at the original institutional repository in a new window.
Providing mechanical support for program development in a weakest precondition calculus
Thesis (MSc)--Stellenbosch University, 1993.
Saved in:
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | Thesis |
| Language: | en_ZA |
| Published: |
Stellenbosch : Stellenbosch University
2013
|
| Subjects: | |
| Tags: |
No Tags, Be the first to tag this record!
|
| _version_ | 1867613994463789056 |
|---|---|
| access_status_str | Open Access |
| author | Ackerman, Charlotte Christene |
| author2 | De Villiers, P. J. A. |
| author_browse | Ackerman, Charlotte Christene De Villiers, P. J. A. |
| author_facet | De Villiers, P. J. A. Ackerman, Charlotte Christene |
| author_sort | Ackerman, Charlotte Christene |
| collection | Thesis |
| dc_rights_str_mv | Stellenbosch University |
| description | Thesis (MSc)--Stellenbosch University, 1993. |
| format | Thesis |
| id | oai:scholar.sun.ac.za:10019.1/79317 |
| institution | Stellenbosch University (South Africa) |
| language | en_ZA |
| last_indexed | 2026-06-10T12:44:59.428Z |
| license_str | Other — see source repository |
| provenance_str_mv | Harvested via OAI-PMH from SUNScholar — Stellenbosch University Repository |
| publishDate | 2013 |
| publishDateRange | 2013 |
| publishDateSort | 2013 |
| publisher | Stellenbosch : Stellenbosch University |
| publisherStr | Stellenbosch : Stellenbosch University |
| record_format | dspace |
| source_str | SUNScholar — Stellenbosch University Repository |
| spelling | oai:scholar.sun.ac.za:10019.1/79317 Providing mechanical support for program development in a weakest precondition calculus Ackerman, Charlotte Christene De Villiers, P. J. A. University of Stellenbosch. Faculty of Science. Dept. of Mathematical Sciences Mathematical logic Calculus -- Computer programs Theses -- Computer science Dissertations -- Computer science Computer software -- Development Thesis (MSc)--Stellenbosch University, 1993. 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. 2013-01-29T10:38:02Z 2013-01-29T10:38:02Z 1993-04 Thesis http://hdl.handle.net/10019.1/79317 en_ZA Stellenbosch University 202 p. application/pdf Stellenbosch : Stellenbosch University |
| spellingShingle | Mathematical logic Calculus -- Computer programs Theses -- Computer science Dissertations -- Computer science Computer software -- Development Ackerman, Charlotte Christene Providing mechanical support for program development in a weakest precondition calculus |
| title | Providing mechanical support for program development in a weakest precondition calculus |
| title_full | Providing mechanical support for program development in a weakest precondition calculus |
| title_fullStr | Providing mechanical support for program development in a weakest precondition calculus |
| title_full_unstemmed | Providing mechanical support for program development in a weakest precondition calculus |
| title_short | Providing mechanical support for program development in a weakest precondition calculus |
| title_sort | providing mechanical support for program development in a weakest precondition calculus |
| topic | Mathematical logic Calculus -- Computer programs Theses -- Computer science Dissertations -- Computer science Computer software -- Development |
| url | http://hdl.handle.net/10019.1/79317 |
| work_keys_str_mv | AT ackermancharlottechristene providingmechanicalsupportforprogramdevelopmentinaweakestpreconditioncalculus |