×

Provably correct derivation of algorithms using FermaT. (English) Zbl 1342.68213

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; Rodin; FermaT; mural
PDFBibTeX XMLCite
Full Text: DOI Link

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 (2009) Invariant based programming: basic approach and teaching experiences. Form Asp Comput 21: 227-244 · Zbl 1178.68334 · doi:10.1007/s00165-008-0070-y
[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 · Zbl 0408.68064
[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 · Zbl 0547.68011
[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 (1977) A transformation system for developing recursive programs. J. Assoc. Comput. Mach. 24: 44-67 · Zbl 0343.68014 · doi:10.1145/321992.321996
[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 (1978) A synthesis of several sort programs. Acta Inform 11: 1-30 · Zbl 0389.68037 · doi:10.1007/BF00264597
[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 0167.46002
[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 (1972) The humble programmer. Commun. ACM 15: 859-866 · doi:10.1145/355604.361591
[19] Gries D (1981) The science of programming. Springer, New York · Zbl 0472.68003 · doi:10.1007/978-1-4612-5983-1
[20] Hoare CAR, Hayes IJ, Jifeng HE, Morgan CC, Roscoe AW, Sanders JW, Sørensen IH, Spivey JM, Sufrin BA (1987) Laws of programming. Commun. ACM 30: 672-686 · Zbl 0629.68006 · doi:10.1145/27651.27653
[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 (1974) Structured programming with the GOTO statement. Comput. Surv. 6: 261-301 · Zbl 0301.68014 · doi:10.1145/356635.356640
[23] Knuth DK (1968) Fundamental algorithms, the art of computer programming #1. Addison Wesley, Reading · Zbl 0191.17903
[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 (1989) The RAISE language, method and tools. Form Asp Comput 1: 85-114 · doi:10.1007/BF01887199
[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 · Zbl 1091.68020
[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 (1971) Program development by stepwise refinement. Commun ACM 14: 221-227 · Zbl 0214.43005 · doi:10.1145/362575.362577
[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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.