乐胖代购免代理版

{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,4]],"date-time":"2023-09-04T17:42:02Z","timestamp":1693849322463},"reference-count":22,"publisher":"Association for Computing Machinery (ACM)","issue":"3","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[1980,7]]},"abstract":"Two approaches to the development of efficient and correct iterative programs are contrasted: the construction of an iterative program and a proof of its correctness using invariant assertions of loops, and the construction and proof of a recursive program with a subsequent transformation into an iterative version by schematically applying suitable recursion removal rules. The connection between the approaches is demonstrated by augmenting such transformation rules by inductive assertions. It is argued that the latter approach to program development is superior since the correctness proof of a recursive program is easier in most cases. Considerable verification overhead can be avoided this way, in particular, some difficulties with the interaction of successive loops and their associated invariants.<\/jats:p>","DOI":"10.1145\/357103.357108","type":"journal-article","created":{"date-parts":[[2002,10,7]],"date-time":"2002-10-07T13:52:47Z","timestamp":1033998767000},"page":"321-337","update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":12,"title":["Derivation of Invariant Assertions During Program Development by Transformation"],"prefix":"10.1145","volume":"2","author":[{"given":"Manfred","family":"Broy","sequence":"first","affiliation":[{"name":"Institut f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen, Postfach 202420, 8000 M\u00fcnchen 2, West Germany"}]},{"given":"Bernd","family":"Krieg-Bruckner","sequence":"additional","affiliation":[{"name":"Computer Science Division--EECS, University of California at Berkeley, Berkeley, CA"}]}],"member":"320","published-online":{"date-parts":[[1980,7]]},"reference":[{"key":"e_1_2_1_1_2","volume-title":"Rapport de Recherche","author":"AMY B.","year":"1978","unstructured":"AMY , B. , AND CAPLAIN , M. Invariances algorithmiques et recurrences . Rapport de Recherche , Grenoble, France , 1978 .]] AMY, B., AND CAPLAIN, M. Invariances algorithmiques et recurrences. Rapport de Recherche, Grenoble, France, 1978.]]"},{"key":"e_1_2_1_2_2","first-page":"75","article-title":"Proving loop programs","volume":"1","author":"BASU S.K.","year":"1975","unstructured":"BASU , S.K. , AND MISRA , J . Proving loop programs . IEEE Trans. Softw. Eng. I , 1 ( 1975 ), 75 - 86 .]] BASU, S.K., AND MISRA, J. Proving loop programs. IEEE Trans. Softw. Eng. I, 1 (1975), 75-86.]]","journal-title":"IEEE Trans. Softw. Eng. I"},{"key":"e_1_2_1_3_2","volume-title":"Proc. IFIP 2nd World Conf., North-Holland Publ. Co.","author":"BAUER F.L.","year":"1975","unstructured":"BAUER , F.L. Top-down teaching of informatics in secondary school. In O. Lecarme and R. Lewis (Eds.) , Proc. IFIP 2nd World Conf., North-Holland Publ. Co. , Amsterdam , 1975 .]] BAUER, F.L. Top-down teaching of informatics in secondary school. In O. Lecarme and R. Lewis (Eds.), Proc. IFIP 2nd World Conf., North-Holland Publ. Co., Amsterdam, 1975.]]"},{"key":"e_1_2_1_4_2","doi-asserted-by":"publisher","DOI":"10.5555\/647446.727072"},{"key":"e_1_2_1_5_2","doi-asserted-by":"publisher","DOI":"10.5555\/800253.807679"},{"key":"e_1_2_1_6_2","first-page":"1","volume-title":"3rd Int. Symp. Programming","author":"BAUER F.L.","year":"1978","unstructured":"BAUER , F.L. , BROY , M. , GNATZ , R. , HESSE , W. , AND KRIEG-BR 0C KNER , B. A wide spectrum language for program development . In 3rd Int. Symp. Programming , Paris , 1978 , pp. 1 - 15 .]] BAUER, F.L., BROY, M., GNATZ, R., HESSE, W., AND KRIEG-BR0CKNER, B. A wide spectrum language for program development. In 3rd Int. Symp. Programming, Paris, 1978, pp. 1-15.]]"},{"key":"e_1_2_1_7_2","first-page":"25","article-title":"Techniques for program development. Software engineering techniques","volume":"34","author":"BAUER F.L.","year":"1977","unstructured":"BAUER , F.L. , PARTSCH , H. , PEPPER , P. , AND WOSSNER , H . Techniques for program development. Software engineering techniques , Infotech State of the Art Rep. 34 , 1977 , pp. 25 - 50 .]] BAUER, F.L., PARTSCH, H., PEPPER, P., AND WOSSNER, H. Techniques for program development. Software engineering techniques, Infotech State of the Art Rep. 34, 1977, pp. 25-50.]]","journal-title":"Infotech State of the Art Rep."},{"key":"e_1_2_1_8_2","unstructured":"BAUER F.L. AND WOSSNER U. Algorithmic languages and program development. To appear.]] BAUER F.L. AND WOSSNER U. Algorithmic languages and program development. To appear.]]"},{"key":"e_1_2_1_9_2","doi-asserted-by":"publisher","DOI":"10.1145\/800168.811550"},{"key":"e_1_2_1_10_2","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_2_1_11_2","volume-title":"Englewood Cliffs","author":"DIJKSTRA E.W.","year":"1976","unstructured":"DIJKSTRA , E.W. A Discipline of Programming. Prentice-HaU , Englewood Cliffs , N.J. , 1976 .]] DIJKSTRA, E.W. A Discipline of Programming. Prentice-HaU, Englewood Cliffs, N.J., 1976.]]"},{"key":"e_1_2_1_12_2","doi-asserted-by":"publisher","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"e_1_2_1_13_2","first-page":"3","article-title":"Proof theory of partial correctness verification systems","volume":"5","author":"GERHART S.L","year":"1976","unstructured":"GERHART , S.L . Proof theory of partial correctness verification systems . SIAJVI J. Comput. 5 , 3 ( 1976 ), 355-377.]] GERHART, S.L. Proof theory of partial correctness verification systems. SIAJVI J. Comput. 5, 3 (1976), 355-377.]]","journal-title":"SIAJVI J. Comput."},{"key":"e_1_2_1_14_2","first-page":"4","article-title":"An illustration of current ideas on the derivation of correctness proofs and correct programs","volume":"2","author":"GRIES D","year":"1976","unstructured":"GRIES , D . An illustration of current ideas on the derivation of correctness proofs and correct programs . IEEE Trans. Softw. Eng. 2 , 4 ( 1976 ), 238-243.]] GRIES, D. An illustration of current ideas on the derivation of correctness proofs and correct programs. IEEE Trans. Softw. Eng. 2, 4 (1976), 238-243.]]","journal-title":"IEEE Trans. Softw. Eng."},{"key":"e_1_2_1_15_2","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_2_1_16_2","doi-asserted-by":"publisher","DOI":"10.1145\/362452.362489"},{"key":"e_1_2_1_17_2","first-page":"5","article-title":"Program optimization using invariants","volume":"4","author":"KATZ S","year":"1978","unstructured":"KATZ , S . Program optimization using invariants . IEEE Trans. Softw. Eng. 4 , 5 ( 1978 ), 378-389.]] KATZ, S. Program optimization using invariants. IEEE Trans. Softw. Eng. 4, 5 (1978), 378-389.]]","journal-title":"IEEE Trans. Softw. Eng."},{"key":"e_1_2_1_18_2","doi-asserted-by":"publisher","DOI":"10.1145\/360032.360048"},{"key":"e_1_2_1_19_2","first-page":"21","volume-title":"Proc. IFIP Congress, 1962","author":"MCCARTHY J.","year":"1962","unstructured":"MCCARTHY , J. Towards a mathematical science of computation . In Proc. IFIP Congress, 1962 . North-Holland Publ. Co., Amsterdam , 1962 , pp. 21 - 28 .]] MCCARTHY, J. Towards a mathematical science of computation. In Proc. IFIP Congress, 1962. North-Holland Publ. Co., Amsterdam, 1962, pp. 21-28.]]"},{"key":"e_1_2_1_20_2","doi-asserted-by":"publisher","DOI":"10.1145\/359461.359466"},{"key":"e_1_2_1_21_2","first-page":"4","article-title":"Induction as basis for program verification","volume":"2","author":"REYNOLDS C.","year":"1976","unstructured":"REYNOLDS , C. , AND YEH , R.T . Induction as basis for program verification . IEEE Trans. Sofiw. Eng. 2 , 4 ( 1976 ), 244-252.]] REYNOLDS, C., AND YEH, R.T. Induction as basis for program verification. IEEE Trans. Sofiw. Eng. 2, 4 (1976), 244-252.]]","journal-title":"IEEE Trans. Sofiw. Eng."},{"key":"e_1_2_1_22_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-0000(71)80036-3"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/357103.357108","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,2]],"date-time":"2023-01-02T10:34:49Z","timestamp":1672655689000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/357103.357108"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1980,7]]},"references-count":22,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1980,7]]}},"alternative-id":["10.1145\/357103.357108"],"URL":"https:\/\/doi.org\/10.1145\/357103.357108","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"value":"0164-0925","type":"print"},{"value":"1558-4593","type":"electronic"}],"subject":[],"published":{"date-parts":[[1980,7]]},"assertion":[{"value":"1980-07-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}