Show simple item record

dc.contributor.authorWard, Martinen
dc.contributor.authorZedan, Husseinen
dc.date.accessioned2013-10-11T09:17:19Z
dc.date.available2013-10-11T09:17:19Z
dc.date.issued2014
dc.identifier.citationWard, M. and Zedan, H. (2014) Provably Correct Derivation of Algorithms Using FermaT. Formal Aspects of Computing, 26 (5), pp. 993-1031en
dc.identifier.urihttp://hdl.handle.net/2086/9173
dc.description.abstractThe transformational programming method of algorithm derivation starts with a formal specification of the result to be achieved, plus some informal ideas as to what techniques will be used in the implementation. The formal specification is then transformed into an implementation, by means of correctness-preserving refinement and transformation steps, guided by the informal ideas. The transformation process will typically include the following stages: (1) Formal specification (2) Elaboration of the specification, (3) Divide and conquer to handle the general case (4) Recursion introduction, (5) Recursion removal, if an iterative solution is desired, (6) Optimisation, if required. At any stage in the process, sub-specifications can be extracted and transformed separately. The main difference between this approach and the invariant based programming approach (and similar stepwise refinement methods) is that loops can be introduced and manipulated while maintaining program correctness and with no need to derive loop invariants. Another difference is that at every stage in the process we are working with a correct program: there is never any need for a separate "verification" step. These factors help to ensure that the method is capable of scaling up to the development of large and complex software systems. The method is applied to the derivation of a complex linked list algorithm and produces code which is over twice as fast as the code written by Donald Knuth to solve the same problem.en
dc.language.isoenen
dc.publisherSpringeren
dc.subjectTransformational Programmingen
dc.subjectFormal Methodsen
dc.subjectSoftware Developmenten
dc.subjectAlgorithm Derivationen
dc.subjectFermaTen
dc.subjectWSLen
dc.titleProvably Correct Derivation of Algorithms Using FermaTen
dc.typeArticleen
dc.identifier.doihttps://dx.doi.org/10.1007/s00165-013-0287-2
dc.researchgroupSoftware Technology Research Laboratory (STRL)en
dc.peerreviewedYesen
dc.funderDe Montfort University and Software Migrations Ltd.en
dc.projectidFermaTen


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record