{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:40:41Z","timestamp":1750308041928,"version":"3.41.0"},"reference-count":19,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2005,6,1]],"date-time":"2005-06-01T00:00:00Z","timestamp":1117584000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["J. Educ. Resour. Comput."],"published-print":{"date-parts":[[2005,6]]},"abstract":"<jats:p>Although computer scientists understand the importance of discrete mathematics to the foundations of their field, computer science (CS) students do not always see the relevance. Thus, it is important to find a way to show students its relevance. The concept of program correctness is generally taught as an activity independent of the programming process, hence many CS students perceive it as unnecessary, and even irrelevant. The concept of contracts, on the other hand, is generally taught as an integral part of the programming process. Most CS students have little difficulty understanding the need to establish contracts via preconditions and postconditions. In order to improve teaching program correctness concepts, we implemented ProVIDE, an enhanced integrated development environment (IDE). ProVIDE assists student programmers in contract construction. Rather than asking for both a precondition and postcondition for each of the student's methods, ProVIDE asks the student to simply supply a postcondition. ProVIDE then helps the student construct the appropriate precondition by leading him or her through an axiomatic proof of the method's correctness. Thus, the proof of of the method's correctness is a side-effect of the student's need to construct an appropriate precondition.<\/jats:p>","DOI":"10.1145\/1141904.1141907","type":"journal-article","created":{"date-parts":[[2006,7,25]],"date-time":"2006-07-25T14:14:26Z","timestamp":1153836866000},"page":"3","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Constructing contracts"],"prefix":"10.1145","volume":"5","author":[{"given":"Timothy S.","family":"Gegg-Harrison","sequence":"first","affiliation":[{"name":"Winona State University, Winona, MN"}]}],"member":"320","published-online":{"date-parts":[[2005,6]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Java Task Force Report: First Public Draft. Internet. Feb.1","author":"ACM JAVA Task Force","year":"2005","unstructured":"ACM JAVA Task Force . 2005. Java Task Force Report: First Public Draft. Internet. Feb.1 , 2005 : http:\/\/cs.stanford.edu\/~eroberts\/\/jtf\/.]] ACM JAVA Task Force. 2005. Java Task Force Report: First Public Draft. Internet. Feb.1, 2005: http:\/\/cs.stanford.edu\/~eroberts\/\/jtf\/.]]"},{"key":"e_1_2_1_2_1","first-page":"2001","article-title":"Computing Curricula 2001","volume":"15","author":"ACM\/IEEE Joint Task Force On Computing Curricula.","year":"2001","unstructured":"ACM\/IEEE Joint Task Force On Computing Curricula. 2001 . Computing Curricula 2001 : Computer Science. Internet . Dec. 15 , 2001 . http:\/\/www.sigcse.org\/cc2001\/.]] ACM\/IEEE Joint Task Force On Computing Curricula. 2001. Computing Curricula 2001: Computer Science. Internet. Dec. 15, 2001. http:\/\/www.sigcse.org\/cc2001\/.]]","journal-title":"Computer Science. Internet"},{"volume-title":"Program Construction and Verification","author":"Backhouse R.W.","key":"e_1_2_1_3_1","unstructured":"Backhouse , R.W. 1986. Program Construction and Verification . Prentice Hall , Englewood Cliffs , N.J.]] Backhouse, R.W. 1986. Program Construction and Verification. Prentice Hall, Englewood Cliffs, N.J.]]"},{"volume-title":"Program Construction: Calculating Implementations from Specifications","author":"Backhouse R.","key":"e_1_2_1_4_1","unstructured":"Backhouse , R. W 2003. Program Construction: Calculating Implementations from Specifications . John Wiley , New York .]] Backhouse, R.W 2003. Program Construction: Calculating Implementations from Specifications. John Wiley, New York.]]"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.5381\/jot.2004.3.6.a2"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/2.774917"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/903893.903918"},{"key":"e_1_2_1_8_1","first-page":"37","article-title":"Why universities require computer science students to take math","volume":"49","author":"Devlin K.","year":"2003","unstructured":"Devlin , K. 2003 . Why universities require computer science students to take math . Commun. ACM 49 ,9, 37 -- 39 .]] Devlin, K. 2003. Why universities require computer science students to take math. Commun. ACM 49,9, 37--39.]]","journal-title":"Commun. ACM"},{"volume-title":"A Discipline of Programming","author":"Dijksktra E.W.","key":"e_1_2_1_9_1","unstructured":"Dijksktra , E.W. 1976. A Discipline of Programming . Prentice Hall , Upper Saddle River, N.J.]] Dijksktra, E.W. 1976. A Discipline of Programming. Prentice Hall, Upper Saddle River, N.J.]]"},{"key":"e_1_2_1_10_1","volume-title":"Proceedings of the 19th Symposium on Applied Mathematics (Mathematical Aspects of Computer Science), American Mathematical Society","author":"Floyd R.W.","year":"1967","unstructured":"Floyd , R.W. 1967 . Assigning meaning to programs . In Proceedings of the 19th Symposium on Applied Mathematics (Mathematical Aspects of Computer Science), American Mathematical Society , Providence, RI.]] Floyd, R.W. 1967. Assigning meaning to programs. In Proceedings of the 19th Symposium on Applied Mathematics (Mathematical Aspects of Computer Science), American Mathematical Society, Providence, RI.]]"},{"key":"e_1_2_1_11_1","volume-title":"Proceedings of the 32nd SIGCSE Technical Symposium on Computer Science Education (SIGCSE","author":"Gegg-Harrison T.S.","year":"2001","unstructured":"Gegg-Harrison , T.S. 2001 . Egyptian numbers: A CS-complete example . In Proceedings of the 32nd SIGCSE Technical Symposium on Computer Science Education (SIGCSE 2001), ACM, New York, 268--272.]] 10.1145\/364447.364598 Gegg-Harrison, T.S. 2001. Egyptian numbers: A CS-complete example. In Proceedings of the 32nd SIGCSE Technical Symposium on Computer Science Education (SIGCSE 2001), ACM, New York, 268--272.]] 10.1145\/364447.364598"},{"key":"e_1_2_1_12_1","volume-title":"Proceedings of the 8th Annual Conference on Innovation and Technology in Computer Science Education (ITiCSE","author":"Gegg-Harrison T.S.","year":"2003","unstructured":"Gegg-Harrison , T.S. , Bunce , G.R. , Ganetzky , R.D. , Olson , C.M. , and Wilson , J.D . 2003. Studying program correctness by constructing contracts . In Proceedings of the 8th Annual Conference on Innovation and Technology in Computer Science Education (ITiCSE 2003 ), ACM, New York, 129--133.]] 10.1145\/961511.961548 Gegg-Harrison, T.S., Bunce, G.R., Ganetzky, R.D., Olson, C.M., and Wilson, J.D. 2003. Studying program correctness by constructing contracts. In Proceedings of the 8th Annual Conference on Innovation and Technology in Computer Science Education (ITiCSE 2003), ACM, New York, 129--133.]] 10.1145\/961511.961548"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46428-X_15"},{"volume-title":"The Science of Programming","author":"Gries D.","key":"e_1_2_1_14_1","unstructured":"Gries , D. 1981. The Science of Programming . Springer-Verlag , New York .]] Gries, D. 1981. The Science of Programming. Springer-Verlag, New York.]]"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/903893.903919"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_2_1_17_1","volume-title":"Proceedings of the 1st International Symposium on Formal Methods for Components and Objects (FMCO","author":"Jacobs B.","year":"2002","unstructured":"Jacobs , B. , Kiniry , J. , and Warnier , M . 2003. Java program verification challenges . In Proceedings of the 1st International Symposium on Formal Methods for Components and Objects (FMCO 2002 ), Springer-Verlag, New York, 202--219.]] Jacobs, B., Kiniry, J., and Warnier, M. 2003. Java program verification challenges. In Proceedings of the 1st International Symposium on Formal Methods for Components and Objects (FMCO 2002), Springer-Verlag, New York, 202--219.]]"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/2.161279"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/129093"}],"container-title":["Journal on Educational Resources in Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1141904.1141907","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1141904.1141907","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T15:14:23Z","timestamp":1750259663000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1141904.1141907"}},"subtitle":["Making discrete mathematics relevant to beginning programmers"],"short-title":[],"issued":{"date-parts":[[2005,6]]},"references-count":19,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2005,6]]}},"alternative-id":["10.1145\/1141904.1141907"],"URL":"https:\/\/doi.org\/10.1145\/1141904.1141907","relation":{},"ISSN":["1531-4278","1531-4278"],"issn-type":[{"type":"print","value":"1531-4278"},{"type":"electronic","value":"1531-4278"}],"subject":[],"published":{"date-parts":[[2005,6]]},"assertion":[{"value":"2005-06-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}