{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,18]],"date-time":"2025-12-18T20:08:08Z","timestamp":1766088488328,"version":"3.43.0"},"reference-count":32,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["2116372"],"award-info":[{"award-number":["2116372"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,8,5]]},"abstract":"<jats:p>A course on software specification deserves a prominent place in the undergraduate curriculum. This report describes our experience teaching a first-year course that places software specification front and center. In support of the course, we created a pedagogic programming language with a focus on contracts and property-based testing. Assignments draw on real-world programs, from a variety of domains, that are intended to show how formal specification can increase confidence in the correctness of code. Interviews with students suggest that this approach successfully conveys how formal specification is relevant to software construction.<\/jats:p>","DOI":"10.1145\/3747533","type":"journal-article","created":{"date-parts":[[2025,8,5]],"date-time":"2025-08-05T16:56:02Z","timestamp":1754412962000},"page":"814-829","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Teaching Software Specification (Experience Report)"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4384-6351","authenticated-orcid":false,"given":"Cameron","family":"Moy","sequence":"first","affiliation":[{"name":"Northeastern University, Boston, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2116-8684","authenticated-orcid":false,"given":"Daniel","family":"Patterson","sequence":"additional","affiliation":[{"name":"Northeastern University, Boston, USA"}]}],"member":"320","published-online":{"date-parts":[[2025,8,5]]},"reference":[{"volume-title":"Principles of Model Checking","author":"Baier Christel","key":"e_1_2_1_1_1","unstructured":"Christel Baier and Joost-Pieter Katoen. 2008. Principles of Model Checking. MIT Press."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","unstructured":"Henry G. Baker. 1993. Equal Rights for Functional Objects or The More Things Change The More They Are The Same. ACM SIGPLAN OOPS Messenger https:\/\/doi.org\/10.1145\/165593.165596 10.1145\/165593.165596","DOI":"10.1145\/165593.165596"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.comnet.2005.01.010"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/214451.214456"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/351240.351266"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","unstructured":"William R. Cook. 2009. On Understanding Data Abstraction Revisited. In Object-Oriented Programming Systems Languages and Applications (OOPSLA). https:\/\/doi.org\/10.1145\/1640089.1640133 10.1145\/1640089.1640133","DOI":"10.1145\/1640089.1640133"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1932681.1863576"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21401-6_26"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.09.018"},{"key":"e_1_2_1_10_1","unstructured":"Carl Eastlund Dale Vaillancourt and Matthias Felleisen. 2007. ACL2 for Freshmen: First Experiences. In ACL2 Workshop."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1017\/s0956796804005076"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1596550.1596561"},{"key":"e_1_2_1_13_1","volume-title":"Matthew Flatt, and Shriram Krishnamurthi.","author":"Felleisen Matthias","year":"2018","unstructured":"Matthias Felleisen, Robert Bruce Findler, Matthew Flatt, and Shriram Krishnamurthi. 2018. How to Design Programs. MIT Press."},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796801004208"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/581478.581484"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3597503.3639581"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3586182.3615788"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1297081.1297089"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","unstructured":"Rich Hickey. 2020. A History of Clojure. In History of Programming Languages (HOPL). https:\/\/doi.org\/10.1145\/3386321 10.1145\/3386321","DOI":"10.1145\/3386321"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICPC66645.2025.00024"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","unstructured":"Casey Klein Matthew Flatt and Robert Bruce Findler. 2010. Random Testing For Higher-Order Stateful Programs. In Object-Oriented Programming Systems Languages and Applications (OOPSLA). https:\/\/doi.org\/10.1145\/1869459.1869505 10.1145\/1869459.1869505","DOI":"10.1145\/1869459.1869505"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","unstructured":"Guillaume Marceau Kathi Fisler and Shriram Krishnamurthi. 2011. Mind Your Language: On Novices\u2019 Interactions With Error Messages. In Onward!. https:\/\/doi.org\/10.1145\/2048237.2048241 10.1145\/2048237.2048241","DOI":"10.1145\/2048237.2048241"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78739-6_2"},{"volume-title":"Object-Oriented Software Construction","author":"Meyer Bertrand","key":"e_1_2_1_24_1","unstructured":"Bertrand Meyer. 1988. Object-Oriented Software Construction. Prentice Hall."},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/44501.45065"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","unstructured":"James H. Morris. 1973. Protection in Programming Languages. Communications of the ACM (CACM) https:\/\/doi.org\/10.1145\/361932.361937 10.1145\/361932.361937","DOI":"10.1145\/361932.361937"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796823000096"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.15653661"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","unstructured":"Rex Page Carl Eastlund and Matthias Felleisen. 2008. Functional Programming and Theorem Proving for Undergraduates: A Progress Report. In Functional and Declarative Programming in Education (FDPE). https:\/\/doi.org\/10.1145\/1411260.1411264 10.1145\/1411260.1411264","DOI":"10.1145\/1411260.1411264"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","unstructured":"D. L. Parnas. 1972. On the Criteria To Be Used in Decomposing Systems into Modules. Communications of the ACM (CACM) https:\/\/doi.org\/10.1145\/361598.361623 10.1145\/361598.361623","DOI":"10.1145\/361598.361623"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.5555\/1247360.1247362"},{"key":"e_1_2_1_32_1","unstructured":"Chihiro Uehara and Kenichi Asai. 2015. Cross Validation of the Universe Teachpack of Racket in OCaml. In Trends in Functional Programming in Education (TFPIE)."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3747533","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,5]],"date-time":"2025-08-05T16:56:04Z","timestamp":1754412964000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3747533"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,8,5]]},"references-count":32,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2025,8,5]]}},"alternative-id":["10.1145\/3747533"],"URL":"https:\/\/doi.org\/10.1145\/3747533","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2025,8,5]]},"assertion":[{"value":"2025-02-27","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-06-27","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-08-05","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}