{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,16]],"date-time":"2025-10-16T03:46:55Z","timestamp":1760586415154},"reference-count":34,"publisher":"Wiley","issue":"3","license":[{"start":{"date-parts":[[2006,10,31]],"date-time":"2006-10-31T00:00:00Z","timestamp":1162252800000},"content-version":"vor","delay-in-days":4686,"URL":"http:\/\/onlinelibrary.wiley.com\/termsAndConditions#vor"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Software Testing Verif &amp; Rel"],"published-print":{"date-parts":[[1994,1]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>This paper describes an approach to the semantic analysis of procedural code. The techniques differ from those adopted in current static analysis tools such as MALPAS (Bramson, 1984) and SPADE (Clutterbuck and Carr\u00e9, 1988) in two key respects: (1) A database is used, together with language\u2010specific and language\u2010independent data models, as a repository for all information about a program or set of programs which is required for analysis, and for storing and interrelating the results of analyses; (2) The techniques aim to treat the full language under consideration by a process of successive transformation and abstraction from the source code until a representation is obtained which is amenable to analysis. This abstraction process can include the production of formal specifications from code. The techniques have been partially implemented for the OS\/VS IBM diallect of COBOL '74 and for FORTRAN '77. Several components of the resulting toolset have been formally specified in Z, thus meeting some of the integrity requirements for verification tools given in \u2018The procurement of safety critical software in defence equipment\u2019 (MoD, 1991). The techniques have been applied in practice to a wide range of source programs and analysis problems (Lano and Haughton, 1993b; Lano, <jats:italic>et al.<\/jats:italic>, 1991), including assessment problems (Lloyd's Register, 1992, 1993; Hornsby and Eldridge, 1990). Section 1 gives an overview of the analysis process. Section 2 describes the representations used to support the process. Section 3 describes some of the techniques involved, and Section 4 gives examples of applications of the process. The Appendix contains extracts from a large case study carried out using tools developed to support the process.<\/jats:p>","DOI":"10.1002\/stvr.4370040304","type":"journal-article","created":{"date-parts":[[2006,11,17]],"date-time":"2006-11-17T16:02:18Z","timestamp":1163779338000},"page":"155-189","source":"Crossref","is-referenced-by-count":9,"title":["Transformational program analysis"],"prefix":"10.1002","volume":"4","author":[{"given":"K.","family":"Lano","sequence":"first","affiliation":[]}],"member":"311","published-online":{"date-parts":[[2006,10,31]]},"reference":[{"key":"e_1_2_1_2_1","volume-title":"Compilers: Principles. Techniques and Tools","author":"Aho A. V.","year":"1986"},{"key":"e_1_2_1_3_1","first-page":"204","volume-title":"Proceedings of Safety Critical Systems Club Meeting","author":"Bennett K.","year":"1994"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2363.2366"},{"key":"e_1_2_1_5_1","unstructured":"Bramson B. D.(1984) \u2018Malvern's Program Analysers \u2019 RSRE Research Review."},{"key":"e_1_2_1_6_1","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1016\/B978-0-934613-12-5.50013-6","volume-title":"Readings in Artificial Intelligence and Software Engineering","author":"Broy M.","year":"1986"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4684-5775-9_8"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1049\/sej.1988.0012"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/0004-3702(81)90014-X"},{"key":"e_1_2_1_10_1","unstructured":"Edwards H. M.andMunro M. (1993) \u2018RECAST: reverse engineering from COBOL to SSADM specification\u2019 inProceedings of the Fifteenth International Conference on Software Engineering Baltimore Maryland U.S.A. May 1993 IEEE Computer Society Press Los Alamitos California U.S.A. pp.499\u2013508."},{"key":"e_1_2_1_11_1","series-title":"McGraw\u2010Hill International Series in Software Engineering","volume-title":"SSADM Version 4: a User's Guide","author":"Eva M.","year":"1992"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/356674.356676"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/52.43050"},{"key":"e_1_2_1_14_1","unstructured":"Horsnby C.andEldridge R.(1990) \u2018Viking pipeline recertification study\u2019 Software Assessement Report Applied Information Engineering 29 Wellesley Rd. Croydon CRO 2AJ. U. K. May 1990."},{"key":"e_1_2_1_15_1","unstructured":"IBM(1970) IBM VS COBOL For OS\/VS IBM Systems Library GC 26\u20103857\u20104."},{"key":"e_1_2_1_16_1","unstructured":"IPSYS Software plc.(1992)IPSYS TBK 2.5.2 Manual (3 Vols) Marlborough Court Pickford Street Macclesfield Cheshire SK11 6JD U. K."},{"key":"e_1_2_1_17_1","unstructured":"Lano K. (1987) \u2018Applications of Prolog to programming semantics\u2019 M. Sc. thesis School of Mathematics University of Bristol Bristol BS8 U. K."},{"key":"e_1_2_1_18_1","unstructured":"Lano K.(1994a) \u2018Specification of real time systems in object\u2010oriented formal methods \u2019 Imperial College 180 Queen's Gate London SW7 2BZ U. K."},{"key":"e_1_2_1_19_1","unstructured":"Lano K.(1994b) \u2018Specifying static analysis tools using formal methods \u2019 Imperial College 180 Queen's Gate London SW7 2BZ U. K."},{"key":"e_1_2_1_20_1","unstructured":"Lano K. Breuer P.andHaughton H.(1991) \u2018Reverse\u2010engineering of library case study\u2019 REDO Project report 2487\u2010TN\u2010PRG\u20101064 Oxford University Programming Research Group 11 Keble Rd. Oxford OX1 3QD U. K."},{"key":"e_1_2_1_21_1","volume-title":"Object\u2010oriented Specification Case Studies","author":"Lano K.","year":"1993"},{"key":"e_1_2_1_22_1","series-title":"McGraw\u2010Hill International Series in Software Engineering","volume-title":"Reverse Engineering and Software Maintenance","author":"Lano K.","year":"1993"},{"key":"e_1_2_1_23_1","unstructured":"Lano K.andOstralenk G.(1993) \u2018The mapping of OS\/VS COBOL into the COBOL schema\u2019 SREDM Project Report DE\u20108 Project Number IED\/4\/1\/3029. Information Engineering Advanced Technology Programme Department of Trade andIndustry U. K."},{"key":"e_1_2_1_24_1","unstructured":"Lloyd's Register(1992) \u2018Assessment and analysis of Horus\u2019 Technical Report CHASE\u2010LR\u201020 v1.0 Applied Information Engineering Lloyd's Register House 29 Wellesley Road Croydon CR0 2AJ U. K. October 1992."},{"key":"e_1_2_1_25_1","unstructured":"Lloyd's Register(1993) \u2018Analysis and documentation of ACT\u2019. Technical Report CHASE\u2010LR\u201036 Applied Information Engineering 29 Wellesley Rd. Croydon CR0 2AJ U. K. April 1993."},{"key":"e_1_2_1_26_1","first-page":"27","volume-title":"Properties of programs and partial function logic\u2019, Machine Intelligence","author":"Manna Z.","year":"1970"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4684-5775-9_10"},{"key":"e_1_2_1_28_1","unstructured":"MoD(1991) \u2018The procurement of safety critical software in defence equipment\u2019 Part 1: \u2018Requirements\u2019 Part 2: \u2018Guidance\u2019 Interim Defence Standard 00\u201355 Issue 1 Ministry of Defence Directorate of Standardization Kentigern House 65 Brown Street Glasgow G2 8EX U. K. 5 April 1991."},{"issue":"2","key":"e_1_2_1_29_1","first-page":"189","article-title":"Assessment of safety\u2010critical software in nuclear power plants","volume":"32","author":"Parnas D.","year":"1991","journal-title":"Nuclear Safety"},{"key":"e_1_2_1_30_1","volume-title":"SPADE semantic analysis course notes","author":"Program Validation Ltd.","year":"1993"},{"key":"e_1_2_1_31_1","series-title":"Hatfield Polytechnic Computing Series","volume-title":"Database Analysis and Design","author":"Robinson H.","year":"1989"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/322033.322034"},{"key":"e_1_2_1_33_1","volume-title":"The REDO Compendium: Reverse Engineering for Software Maintenance","author":"van Zuylen H.","year":"1992"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1984.5010248"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/21.2.161"}],"container-title":["Software Testing, Verification and Reliability"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.wiley.com\/onlinelibrary\/tdm\/v1\/articles\/10.1002%2Fstvr.4370040304","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/pdf\/10.1002\/stvr.4370040304","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,10,24]],"date-time":"2023-10-24T00:13:25Z","timestamp":1698106405000},"score":1,"resource":{"primary":{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/10.1002\/stvr.4370040304"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994,1]]},"references-count":34,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1994,1]]}},"alternative-id":["10.1002\/stvr.4370040304"],"URL":"https:\/\/doi.org\/10.1002\/stvr.4370040304","archive":["Portico"],"relation":{},"ISSN":["0960-0833","1099-1689"],"issn-type":[{"value":"0960-0833","type":"print"},{"value":"1099-1689","type":"electronic"}],"subject":[],"published":{"date-parts":[[1994,1]]}}}