{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,11,19]],"date-time":"2023-11-19T13:42:40Z","timestamp":1700401360111},"reference-count":15,"publisher":"Wiley","issue":"2","license":[{"start":{"date-parts":[[2002,1,28]],"date-time":"2002-01-28T00:00:00Z","timestamp":1012176000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/summer-heart-0930.chufeiyun1688.workers.dev:443\/http\/onlinelibrary.wiley.com\/termsAndConditions#vor"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Software Testing Verif &amp; Rel"],"published-print":{"date-parts":[[2002,6]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Earlier work suggests that program transformations can simplify program verification. A given program containing complex language features is transformed into a semantically equivalent program containing only simpler language features. The transformed program is proven using a set of proof rules for only the simpler features. That approach was illustrated by transforming a given program that may contain multiple\u2010level escape statements within nested loops into an equivalent program that contains no escape statements. This paper gives additional transformations, which map a given program that may contain multiple\u2010level escape statements to a semantically equivalent program (<jats:italic>TP<\/jats:italic>) that contains only single\u2010level escape statements. The proof of <jats:italic>TP<\/jats:italic> uses proof rules for single\u2010level escape statements, or the earlier transformations further map <jats:italic>TP<\/jats:italic> to a program with no escape statements, whose proof uses proof rules for loops without escape statements. This paper also discusses escape statements where the number of levels is determined at run\u2010time. Copyright \u00a9 2002 John Wiley &amp; Sons, Ltd.<\/jats:p>","DOI":"10.1002\/stvr.236","type":"journal-article","created":{"date-parts":[[2002,10,6]],"date-time":"2002-10-06T12:27:22Z","timestamp":1033907242000},"page":"71-76","source":"Crossref","is-referenced-by-count":1,"title":["Additional transformations for multiple\u2010level escape statements"],"prefix":"10.1002","volume":"12","author":[{"given":"Ronald A.","family":"Olsson","sequence":"first","affiliation":[]}],"member":"311","published-online":{"date-parts":[[2002,1,28]]},"reference":[{"key":"e_1_2_1_2_2","doi-asserted-by":"publisher","DOI":"10.1002\/(SICI)1099-1689(199906)9:2<85::AID-STVR178>3.0.CO;2-2"},{"key":"e_1_2_1_3_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00260921"},{"key":"e_1_2_1_4_2","volume-title":"The C Programming Language","author":"Kernighan BW","year":"1978"},{"key":"e_1_2_1_5_2","volume-title":"The C++ Programming Language","author":"Stroustrup B","year":"1985"},{"key":"e_1_2_1_6_2","series-title":"Java Series","volume-title":"The Java Language Specification","author":"Gosling J","year":"1996"},{"key":"e_1_2_1_7_2","unstructured":"American National Standards Institute.Reference Manual for the Ada Programming Language 1983. ANSI\/MIL\u2010STD\u20101815A."},{"key":"e_1_2_1_8_2","doi-asserted-by":"publisher","DOI":"10.1145\/954666.971189"},{"key":"e_1_2_1_9_2","doi-asserted-by":"publisher","DOI":"10.1145\/53580.53581"},{"key":"e_1_2_1_10_2","doi-asserted-by":"publisher","DOI":"10.1145\/42192.42324"},{"key":"e_1_2_1_11_2","volume-title":"The SR Programming Language: Concurrency in Practice","author":"Andrews GR","year":"1993"},{"key":"e_1_2_1_12_2","doi-asserted-by":"publisher","DOI":"10.1145\/360933.360975"},{"key":"e_1_2_1_13_2","volume-title":"A Discipline of Programming","author":"Dijkstra EW","year":"1976"},{"key":"e_1_2_1_14_2","unstructured":"American National Standards Institute New York City NY.American National Standard FORTRAN (ANS X3.9\u20101966).1966."},{"key":"e_1_2_1_15_2","doi-asserted-by":"publisher","DOI":"10.1145\/356561.356564"},{"key":"e_1_2_1_16_2","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(91)90058-P"}],"container-title":["Software Testing, Verification and Reliability"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/summer-heart-0930.chufeiyun1688.workers.dev:443\/https\/api.wiley.com\/onlinelibrary\/tdm\/v1\/articles\/10.1002%2Fstvr.236","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/summer-heart-0930.chufeiyun1688.workers.dev:443\/https\/onlinelibrary.wiley.com\/doi\/pdf\/10.1002\/stvr.236","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,11,19]],"date-time":"2023-11-19T13:15:15Z","timestamp":1700399715000},"score":1,"resource":{"primary":{"URL":"https:\/\/summer-heart-0930.chufeiyun1688.workers.dev:443\/https\/onlinelibrary.wiley.com\/doi\/10.1002\/stvr.236"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,1,28]]},"references-count":15,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2002,6]]}},"alternative-id":["10.1002\/stvr.236"],"URL":"https:\/\/summer-heart-0930.chufeiyun1688.workers.dev:443\/https\/doi.org\/10.1002\/stvr.236","archive":["Portico"],"relation":{},"ISSN":["0960-0833","1099-1689"],"issn-type":[{"value":"0960-0833","type":"print"},{"value":"1099-1689","type":"electronic"}],"subject":[],"published":{"date-parts":[[2002,1,28]]}}}