×

zbMATH — the first resource for mathematics

Provably correct derivation of algorithms using FermaT. (English) Zbl 1342.68213
Summary: The 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.
MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
68N19 Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.)
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
Software:
RAISE; FermaT; Rodin; mural
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] ISO JTC 1/SC 7 (2006) Software engineering—software life cycle processes—maintenance. ISO/IEC 14764:2006
[2] Abrial J-R, Butler M, Hallerstede S, Voisin L (2006) An open extensible tool environment for Event-B. ICFEM, New York
[3] Back, R-J, Invariant based programming: basic approach and teaching experiences, Form Asp Comput, 21, 227-244, (2009) · Zbl 1178.68334
[4] Bauer FL (1979) Program development by stepwise transformations—the project CIP. In: Goos G, Hartmanis H (eds) Program construction. Lecture Notes in Computer Science. #69, Springer, New York, pp 237-266
[5] Bauer FL, Berghammer R et al, The CIP Language Group (1985) The Munich Project CIP. Volume I: the wide spectrum language CIP-L. Lecture Notes in Computer Science #183, Springer, New York · Zbl 0572.68010
[6] Bauer FL, Moller B, Partsch H, Pepper P (1989) Formal construction by transformation—computer aided intuition guided programming. IEEE Trans Softw Eng 15 #2 · Zbl 0664.68017
[7] Bauer FL, The CIP System Group (1987) The Munich Project CIP, Volume II: the program transformation system CIP-S. Lecture Notes in Computer Science #292, Springer, New York · Zbl 0645.68004
[8] Bicarregui JC, Matthews BM (1999) Proof and refutation in formal software development. In: 3rd Irish workshop on formal software development
[9] Bird R, de Moor O (1996) The algebra of programming. Prentice-Hall, Englewood Cliffs · Zbl 0847.68014
[10] Broy M (1984) Algebraic methods for program construction: the project CIP. In: Pepper P (ed) Program transformation and programming environments report on a workshop directed by F. L. Bauer and H. Remus. Springer, New York, pp 199-222
[11] Bundy A, Grov G, Lin Y (2011) Productive use of failure in top-down formal methods. In: Automated reasoning workshop ARW 2011, Glasgow, 11th-12th April · Zbl 0389.68037
[12] Burstall, RM; Darlington, JA, A transformation system for developing recursive programs, J. Assoc. Comput. Mach., 24, 44-67, (1977) · Zbl 0343.68014
[13] Butler M (2006) On the verified-by-construction approach. BCS FACS, Electronics & Computer Science EPrints Service, oai:eprints.soton.ac.uk:265110 · Zbl 0343.68014
[14] Darlington, J, A synthesis of several sort programs, Acta Inform, 11, 1-30, (1978) · Zbl 0389.68037
[15] Dijkstra EW. A constructive approach to the problem of program correctness. Technische Hogeschool Eindhoven, EWD209. http://www.cs.utexas.edu/users/EWD/ewd02xx/EWD209.PDF · Zbl 1178.68334
[16] Dijkstra EW (1976) A discipline of programming. Prentice-Hall, Englewood Cliffs · Zbl 0368.68005
[17] Dijkstra EW (1970) Notes on structured programming. Technische Hogeschool Eindhoven, EWD249. http://www.cs.utexas.edu/users/EWD/ewd02xx/EWD249.PDF
[18] Dijkstra, EW, The humble programmer, Commun. ACM, 15, 859-866, (1972)
[19] Gries D (1981) The science of programming. Springer, New York · Zbl 0472.68003
[20] Hoare, CAR; Hayes, IJ; Jifeng, HE; Morgan, CC; Roscoe, AW; Sanders, JW; Sørensen, IH; Spivey, JM; Sufrin, BA, Laws of programming, Commun. ACM, 30, 672-686, (1987) · Zbl 0629.68006
[21] Jones CB, Jones KD, Lindsay PA, Moore R (1991) mural: A formal development support system. Springer, New York · Zbl 0758.68046
[22] Knuth, DE, Structured programming with the GOTO statement, Comput. Surv., 6, 261-301, (1974) · Zbl 0301.68014
[23] Knuth DK (1968) Fundamental algorithms, the art of computer programming #1. Addison Wesley, Reading
[24] Leiserson CE, Prokop H, Randall KH (1998) Using de Bruijn Sequences to Index a 1 in a Computer Word. CiteSeer. http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.37.8562
[25] Morgan CC (1994) Programming from specifications, 2nd edn. Prentice-Hall, Englewood Cliffs · Zbl 0829.68083
[26] Morgan CC, Robinson K, Gardiner P (1988) On the refinement calculus. Technical Monograph PRG-70. Oxford University, Oxford
[27] Morgan CC, Vickers T (1993) On the refinement calculus. Springer, New York
[28] Neilson, M; Havelund, K; Wagner, KR; Saaman, E, The RAISE language, method and tools, Form Asp Comput, 1, 85-114, (1989)
[29] Priestley HA, Ward M (1994) A multipurpose backtracking algorithm. J Symb Comput 18:1-40. http://www.cse.dmu.ac.uk/ mward/martin/papers/backtr-t.ps.gz doi:10.1006/jsco.1994.1035
[30] Sennett CT (1990) Using refinement to convince: lessons learned from a case study. Refinement workshop, 8th-11th January, Hursley Park, Winchester
[31] Tammet T (1995) Lambda lifting as an optimization for compiling Scheme to C. Chalmers University of Technology, Department of Computer Sciences, Goteborg, Sweden. ftp://ftp.cs.chalmers.se/pub/users/tammet/hobbit.ps
[32] Thomas M (2003) The modest software engineer In: Sixth international symposium on autonomous decentralized systems, ISADS
[33] Ward M (1989) Proving program refinements and transformations. Oxford University, DPhil Thesis. http://www.cse.dmu.ac.uk/ mward/martin/thesis
[34] Ward M (1990) Derivation of a sorting algorithm. Durham University, Technical Report. http://www.cse.dmu.ac.uk/ mward/martin/papers/sorting-t.ps.gz
[35] Ward M (1994) Reverse engineering through formal transformation knuths “polynomial addition” Algorithm Comput J 37:795-813. http://www.cse.dmu.ac.uk/ mward/martin/papers/poly-t.ps.gz. doi:10.1093/comjnl/37.9.795
[36] Ward M (1996) Program analysis by formal transformation. Comput J 39. http://www.cse.dmu.ac.uk/ mward/martin/papers/topsort-t.ps.gz. doi:10.1093/comjnl/39.7.598
[37] Ward M (1999) Recursion removal/introduction by formal transformation: an aid to program development and program comprehension. Comput J 42:650-673. http://www.cse.dmu.ac.uk/ mward/martin/papers/recursion-t.ps.gz. doi:10.1093/comjnl/42.8.650 · Zbl 0956.68014
[38] Ward M (1999) Assembler to C migration using the FermaT transformation system. In: International conference on software maintenance, 30th Aug-3rd Sept 1999, Oxford, England · Zbl 1178.68334
[39] Ward M (1993) Abstracting a specification from code. J Softw Maint Res Pract 5:101-122. http://www.cse.dmu.ac.uk/ mward/martin/papers/prog-spec.ps.gz
[40] Ward M (1996) Derivation of data intensive algorithms by formal transformation. IEEE Trans Softw Eng 22:665-686. http://www.cse.dmu.ac.uk/ mward/martin/papers/sw-alg.ps.gz, http://doi.ieeecomputersociety.org/10.1109/32.541437
[41] Ward M (2001) The FermaT assembler re-engineering workbench. In: International conference on software maintenance (ICSM), 6th-9th November 2001, Florence, Italy
[42] Ward M (2004) Pigs from sausages? Reengineering from assembler to C via FermaT transformations. Sci Comput Progr Spec Issue Progr Transform 52:213-255. http://www.cse.dmu.ac.uk/ mward/martin/papers/migration-t.ps.gz, http://dx.doi.org/10.1016/j.scico.2004.03.007
[43] Ward M, Zedan H (2005) MetaWSL and meta-transformations in the FermaT transformation system. In: 29th Annual international computer software and applications conference, Edinburgh, UK, November 2005
[44] Ward M, Zedan H (2007) Slicing as a program transformation. Trans Progr Lang Syst 29:1-52. http://www.cse.dmu.ac.uk/ mward/martin/papers/slicing-t.ps.gz, http://doi.acm.org/10.1145/1216374.1216375
[45] Ward M, Zedan H (2010) Deriving a slicing algorithm via FermaT transformations. IEEE Trans Softw Eng IEEE Comput Soc Digit Libr. http://www.cse.dmu.ac.uk/ mward/martin/papers/derivation2-a4-t.pdf, http://doi.ieeecomputersociety.org/10.1109/TSE.2010.13
[46] Ward M, Zedan H, Hardcastle T (2004) Legacy assembler reengineering and migration. In: 20th IEEE international conference on software maintenance, 11th-17th Sept, Chicago, Illinois, USA · Zbl 0214.43005
[47] Ward M, Zedan H, Ladkau M, Natelberg S (2008) Conditioned semantic slicing for abstraction; industrial experiment. Softw Pract Exp 38:1273-1304. http://www.cse.dmu.ac.uk/ mward/martin/papers/slicing-paper-final.pdf, http://doi.wiley.com/10.1002/spe.869
[48] Wirth, N, Program development by stepwise refinement, Commun ACM, 14, 221-227, (1971) · Zbl 0214.43005
[49] Yang H, Ward M (2003) Successful evolution of software systems. Artech House, Boston, London. ISBN-10 1-58053-349-3. ISBN-13 978-1580533492 · Zbl 0343.68014
[50] Zhang X, Munro M, Harman M, Hu L (2002) Mechanized operational semantics of WSL. In: IEEE international workshop on source code analysis and manipulation (SCAM), Los Alamitos, California, USA
[51] Zhang X, Munro M, Harman M, Hu L (2002) Weakest precondition for general recursive programs formalized in coq. Lecture Notes in Computer Science. In: Proceedings of the 15th international conference on theorem proving in higher order logics (TPHOLs). Springer, New York · Zbl 1013.68202
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.