{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,8,27]],"date-time":"2023-08-27T08:50:56Z","timestamp":1693126256020},"reference-count":14,"publisher":"Association for Computing Machinery (ACM)","issue":"2","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["SIGCSE Bull."],"published-print":{"date-parts":[[2009,6,25]]},"abstract":"The Event B modelling language provides a framework for teaching programming methodology based on the famous pre\/post-specifications, together with the refinement. We illustrate the call-as-event pattern for helping users to use Event B. As teacher, we are using students to evaluate our methodology and we give comments in italic, when we have got reactions from our students: a given definition, a concept related to our methodology, for instance. We discuss points related to our lectures at different levels of the university, mainly master. Simple case studies illustrate the teaching methodology based on interactive proofs.<\/jats:p>","DOI":"10.1145\/1595453.1595462","type":"journal-article","created":{"date-parts":[[2009,8,24]],"date-time":"2009-08-24T14:08:31Z","timestamp":1251122911000},"page":"51-59","update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["A simple refinement-based method for constructing algorithms"],"prefix":"10.1145","volume":"41","author":[{"given":"Dominique","family":"M\u00e9ry","sequence":"first","affiliation":[{"name":"Universit\u00e9 Henri Poincar\u00e9 Nancy 1, Vandoeuvre-l\u00e8s-Nancy, France"}]}],"member":"320","published-online":{"date-parts":[[2009,6,25]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511624162","volume-title":"The B book - Assigning Programs to Meanings","author":"Abrial J.-R.","year":"1996","unstructured":"Abrial , J.-R. The B book - Assigning Programs to Meanings . Cambridge University Press , 1996 . Abrial, J.-R. The B book - Assigning Programs to Meanings. Cambridge University Press, 1996."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/1761968.1761980"},{"key":"e_1_2_1_3_1","first-page":"51","article-title":"Event based sequential program development: Application to constructing a pointer program","volume":"2003","author":"Abrial J.-R","year":"2003","unstructured":"Abrial , J.-R . Event based sequential program development: Application to constructing a pointer program . In Fme 2003 ( 2003 ), pp. 51 -- 74 . Abrial, J.-R. Event based sequential program development: Application to constructing a pointer program. In Fme 2003 (2003), pp. 51--74.","journal-title":"Fme"},{"key":"e_1_2_1_4_1","first-page":"1","article-title":"Click'n prove: Interactive proofs within set theory","volume":"2003","author":"Abrial J.-R.","year":"2003","unstructured":"Abrial , J.-R. , and Cansell , D . Click'n prove: Interactive proofs within set theory . In Tphol 2003 ( 2003 ), pp. 1 -- 24 . Abrial, J.-R., and Cansell, D. Click'n prove: Interactive proofs within set theory. In Tphol 2003 (2003), pp. 1--24.","journal-title":"Tphol"},{"key":"e_1_2_1_5_1","first-page":"1","article-title":"On correct refinement of programs","volume":"23","author":"Back R","year":"1979","unstructured":"Back , R . On correct refinement of programs . Journal of Computer and System Sciences 23 , 1 ( 1979 ), 49--68. Back, R. On correct refinement of programs. Journal of Computer and System Sciences 23, 1 (1979), 49--68.","journal-title":"Journal of Computer and System Sciences"},{"key":"e_1_2_1_6_1","first-page":"33","volume-title":"The event-B Modelling Method: Concepts and Case Studies","author":"Cansell D.","year":"2007","unstructured":"Cansell , D. , and Mery , D . The event-B Modelling Method: Concepts and Case Studies . Springer , 2007 , pp. 33 -- 140 . See {?}. Cansell, D., and Mery, D. The event-B Modelling Method: Concepts and Case Studies. Springer, 2007, pp. 33--140. See {?}."},{"key":"e_1_2_1_7_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"104","DOI":"10.1007\/978-3-540-74510-5_13","volume-title":"CSR","author":"Cansell D.","year":"2007","unstructured":"Cansell , D. , and Mery , D . Proved-patterns-based development for structured programs . In CSR ( 2007 ), V. Diekert, M.V. Volkov, and A. Voronkov, Eds., vol. 4649 of Lecture Notes in Computer Science , Springer , pp. 104 -- 114 . Cansell, D., and Mery, D. Proved-patterns-based development for structured programs. In CSR (2007), V. Diekert, M.V. Volkov, and A. Voronkov, Eds., vol. 4649 of Lecture Notes in Computer Science, Springer, pp. 104--114."},{"key":"e_1_2_1_8_1","volume-title":"A Discipline of Programming","author":"Dijkstra E.W.","year":"1976","unstructured":"Dijkstra , E.W. A Discipline of Programming . Prentice-Hall , 1976 . Dijkstra, E.W. A Discipline of Programming. Prentice-Hall, 1976."},{"key":"e_1_2_1_9_1","volume-title":"Untersuchungen Uber das Logische Schliessen ou Recherches sur la d&#233;duction loqique","author":"Gentzen G.","year":"1955","unstructured":"Gentzen , G. Untersuchungen Uber das Logische Schliessen ou Recherches sur la d&#233;duction loqique . 1955 . Traduction de Feys et Ladriere . Gentzen, G. Untersuchungen Uber das Logische Schliessen ou Recherches sur la d&#233;duction loqique. 1955. Traduction de Feys et Ladriere."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1173706.1173740"},{"key":"e_1_2_1_12_1","volume-title":"Programming from Specifications","author":"Morgan C.","year":"1990","unstructured":"Morgan , C. Programming from Specifications . Prentice Hall International Series in Computer Science. Prentice Hall , 1990 . Morgan, C. Programming from Specifications. Prentice Hall International Series in Computer Science. Prentice Hall, 1990."},{"key":"e_1_2_1_13_1","volume-title":"The B Method: from Research to Teaching (June","author":"Mery D.","year":"2008","unstructured":"Mery , D. Teaching programming methodology using event b . In The B Method: from Research to Teaching (June 2008 ), H. Habrias , Ed . Mery, D. Teaching programming methodology using event b. In The B Method: from Research to Teaching (June 2008), H. Habrias, Ed."},{"key":"e_1_2_1_14_1","unstructured":"Project Rodin. Rigorous open development environment for complex systems. http:\/\/rodin-b-sharp.sourceforge.net\/ 2004. 2004-2007. Project Rodin. Rigorous open development environment for complex systems. http:\/\/rodin-b-sharp.sourceforge.net\/ 2004. 2004-2007."}],"container-title":["ACM SIGCSE Bulletin"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1595453.1595462","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,29]],"date-time":"2022-12-29T07:45:40Z","timestamp":1672299940000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1595453.1595462"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,6,25]]},"references-count":14,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2009,6,25]]}},"alternative-id":["10.1145\/1595453.1595462"],"URL":"https:\/\/doi.org\/10.1145\/1595453.1595462","relation":{},"ISSN":["0097-8418"],"issn-type":[{"value":"0097-8418","type":"print"}],"subject":[],"published":{"date-parts":[[2009,6,25]]},"assertion":[{"value":"2009-06-25","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}