{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,31]],"date-time":"2025-08-31T23:25:00Z","timestamp":1756682700372,"version":"3.40.3"},"publisher-location":"Cham","reference-count":31,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031711763"},{"type":"electronic","value":"9783031711770"}],"license":[{"start":{"date-parts":[[2024,9,13]],"date-time":"2024-09-13T00:00:00Z","timestamp":1726185600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,9,13]],"date-time":"2024-09-13T00:00:00Z","timestamp":1726185600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Platforms to support novices learning to program are often accompanied by automated next-step hints that guide them towards correct solutions. Many of those approaches are data-driven, building on historical data to generate higher quality hints. Formal specifications are increasingly relevant in software engineering activities, but very little support exists to help novices while learning. Alloy is a formal specification language often used in courses on formal software development methods, and a platform\u2014Alloy4Fun\u2014has been proposed to support autonomous learning. While non-data-driven specification repair techniques have been proposed for Alloy that could be leveraged to generate next-step hints, no data-driven hint generation approach has been proposed so far. This paper presents the first data-driven hint generation technique for Alloy and its implementation as an extension to Alloy4Fun, being based on the data collected by that platform. This historical data is processed into graphs that capture past students\u2019 progress while solving specification challenges. Hint generation can be customized with policies that take into consideration diverse factors, such as the popularity of paths in those graphs successfully traversed by previous students. Our evaluation shows that the performance of this new technique is competitive with non-data-driven repair techniques. To assess the quality of the hints, and help select the most appropriate hint generation policy, we conducted a survey with experienced Alloy instructors.<\/jats:p>","DOI":"10.1007\/978-3-031-71177-0_8","type":"book-chapter","created":{"date-parts":[[2024,9,12]],"date-time":"2024-09-12T06:10:51Z","timestamp":1726121451000},"page":"104-121","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Alloy Repair Hint Generation Based on\u00a0Historical Data"],"prefix":"10.1007","author":[{"given":"Ana","family":"Barros","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0001-2701-7318","authenticated-orcid":false,"given":"Henrique","family":"Neto","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2714-8027","authenticated-orcid":false,"given":"Alcino","family":"Cunha","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4817-948X","authenticated-orcid":false,"given":"Nuno","family":"Macedo","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3431-8060","authenticated-orcid":false,"given":"Ana C. R.","family":"Paiva","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,9,13]]},"reference":[{"issue":"1","key":"8_CR1","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1007\/s40593-015-0089-1","volume":"26","author":"V Aleven","year":"2016","unstructured":"Aleven, V., Roll, I., McLaren, B.M., Koedinger, K.R.: Help helps, but only so much: Research on help seeking with intelligent tutoring systems. Int. J. Artif. Intell. Educ. 26(1), 205\u2013223 (2016)","journal-title":"Int. J. Artif. Intell. Educ."},{"key":"8_CR2","doi-asserted-by":"publisher","unstructured":"Barnes, T., Stamper, J.C.: Toward automatic hint generation for logic proof tutoring using historical student data. In: ITS, LNCS, vol.\u00a05091, pp. 373\u2013382. Springer (2008). https:\/\/doi.org\/10.1007\/978-3-540-69132-7_41","DOI":"10.1007\/978-3-540-69132-7_41"},{"key":"8_CR3","doi-asserted-by":"crossref","unstructured":"Brida, S.G., et al.: Bounded exhaustive search of Alloy specification repairs. In: ICSE, pp. 1135\u20131147. IEEE (2021)","DOI":"10.1109\/ICSE43902.2021.00105"},{"key":"8_CR4","doi-asserted-by":"publisher","unstructured":"Cerqueira, J., Cunha, A., Macedo, N.: Timely specification repair for Alloy 6. In: SEFM, LNCS, vol. 13550, pp. 288\u2013303. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-17108-6_18","DOI":"10.1007\/978-3-031-17108-6_18"},{"key":"8_CR5","doi-asserted-by":"crossref","unstructured":"Chawathe, S.S., Rajaraman, A., Garcia-Molina, H., Widom, J.: Change detection in hierarchically structured information. In: SIGMOD Conference, pp. 493\u2013504. ACM Press (1996)","DOI":"10.1145\/235968.233366"},{"key":"8_CR6","doi-asserted-by":"crossref","unstructured":"Cunha, A., Macedo, N., Campos, J.C., Margolis, I., Sousa, E.: Assessing the impact of hints in learning formal specification. In: SEET@ICSE, pp. 151\u2013161. ACM (2024)","DOI":"10.1145\/3639474.3640050"},{"key":"8_CR7","doi-asserted-by":"publisher","unstructured":"Danas, N., Nelson, T., Harrison, L., Krishnamurthi, S., Dougherty, D.J.: User studies of principled model finder output. In: SEFM, LNCS, vol. 10469, pp. 168\u2013184. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-66197-1_11","DOI":"10.1007\/978-3-319-66197-1_11"},{"issue":"OOPSLA1","key":"8_CR8","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3527323","volume":"6","author":"T Dyer","year":"2022","unstructured":"Dyer, T., Nelson, T., Fisler, K., Krishnamurthi, S.: Applying cognitive principles to model-finding output: the positive value of negative information. Proc. ACM Program. Lang. 6(OOPSLA1), 1\u201329 (2022)","journal-title":"Proc. ACM Program. Lang."},{"key":"8_CR9","doi-asserted-by":"crossref","unstructured":"Falleri, J., Morandat, F., Blanc, X., Martinez, M., Monperrus, M.: Fine-grained and accurate source code differencing. In: ASE, pp. 313\u2013324. ACM (2014)","DOI":"10.1145\/2642937.2642982"},{"key":"8_CR10","doi-asserted-by":"crossref","unstructured":"Gusukuma, L., Bart, A.C., Kafura, D.G., Ernst, J.: Misconception-driven feedback: results from an experimental study. In: ICER, pp. 160\u2013168. ACM (2018)","DOI":"10.1145\/3230977.3231002"},{"key":"8_CR11","doi-asserted-by":"publisher","unstructured":"Hicks, A., Peddycord III, B.W., Barnes, T.: Building games to learn from their players: generating hints in a serious game. In: ITS, LNCS, vol.\u00a08474, pp. 312\u2013317. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-07221-0_39","DOI":"10.1007\/978-3-319-07221-0_39"},{"key":"8_CR12","unstructured":"Jackson, D.: Software abstractions: Logic, language, and analysis. MIT Press, revised edn. (2006)"},{"issue":"9","key":"8_CR13","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1145\/3338843","volume":"62","author":"D Jackson","year":"2019","unstructured":"Jackson, D.: Alloy: a language and tool for exploring software designs. Commun. ACM 62(9), 66\u201376 (2019)","journal-title":"Commun. ACM"},{"issue":"4","key":"8_CR14","doi-asserted-by":"publisher","first-page":"429","DOI":"10.1109\/TLT.2017.2743701","volume":"11","author":"T Lazar","year":"2018","unstructured":"Lazar, T., Sadikov, A., Bratko, I.: Rewrite rules for debugging student programs in programming tutors. IEEE Trans. Learn. Technol. 11(4), 429\u2013440 (2018)","journal-title":"IEEE Trans. Learn. Technol."},{"key":"8_CR15","doi-asserted-by":"publisher","unstructured":"Macedo, N., Cunha, A., Paiva, A.C.R.: Alloy4Fun dataset for 2022\/23 (2023). https:\/\/doi.org\/10.5281\/zenodo.8123547, https:\/\/doi.org\/10.5281\/zenodo.8123547","DOI":"10.5281\/zenodo.8123547"},{"key":"8_CR16","doi-asserted-by":"publisher","first-page":"102690","DOI":"10.1016\/j.scico.2021.102690","volume":"211","author":"N Macedo","year":"2021","unstructured":"Macedo, N., et al.: Experiences on teaching Alloy with an automated assessment platform. Sci. Comput. Program. 211, 102690 (2021)","journal-title":"Sci. Comput. Program."},{"key":"8_CR17","doi-asserted-by":"crossref","unstructured":"Mansoor, N., Bagheri, H., Kang, E., Sharif, B.: An empirical study assessing software modeling in Alloy. In: FormaliSE. pp. 44\u201354. IEEE (2023)","DOI":"10.1109\/FormaliSE58978.2023.00013"},{"key":"8_CR18","doi-asserted-by":"crossref","unstructured":"Marwan, S., Lytle, N., Williams, J.J., Price, T.W.: The impact of adding textual explanations to next-step hints in a novice programming environment. In: ITiCSE, pp. 520\u2013526. ACM (2019)","DOI":"10.1145\/3304221.3319759"},{"issue":"3","key":"8_CR19","doi-asserted-by":"publisher","first-page":"399","DOI":"10.1109\/TLT.2022.3223577","volume":"16","author":"S Marwan","year":"2023","unstructured":"Marwan, S., Price, T.W.: iSnap: evolution and evaluation of a data-driven hint system for block-based programming. IEEE Trans. Learn. Technol. 16(3), 399\u2013413 (2023)","journal-title":"IEEE Trans. Learn. Technol."},{"key":"8_CR20","doi-asserted-by":"crossref","unstructured":"Marwan, S., Williams, J.J., Price, T.W.: An evaluation of the impact of automated programming hints on performance and learning. In: ICER, pp. 61\u201370. ACM (2019)","DOI":"10.1145\/3291279.3339420"},{"key":"8_CR21","doi-asserted-by":"crossref","unstructured":"McBroom, J., Koprinska, I., Yacef, K.: A survey of automated programming hint generation: the hints framework. ACM Comput. Surv. 54(8), 1\u201327 (2022)","DOI":"10.1145\/3469885"},{"key":"8_CR22","doi-asserted-by":"crossref","unstructured":"Piech, C., Sahami, M., Huang, J., Guibas, L.J.: Autonomously generating hints by inferring problem solving policies. In: L@S, pp. 195\u2013204. ACM (2015)","DOI":"10.1145\/2724660.2724668"},{"key":"8_CR23","unstructured":"Price, T.W., Dong, Y., Barnes, T.: Generating data-driven hints for open-ended programming. In: EDM, pp. 191\u2013198. Int. Educ. Data Min. Soc. (IEDMS) (2016)"},{"issue":"3","key":"8_CR24","doi-asserted-by":"publisher","first-page":"368","DOI":"10.1007\/s40593-019-00177-z","volume":"29","author":"TW Price","year":"2019","unstructured":"Price, T.W., et al.: A comparison of the quality of data-driven programming hint generation algorithms. Int. J. Artif. Intell. Educ. 29(3), 368\u2013395 (2019)","journal-title":"Int. J. Artif. Intell. Educ."},{"key":"8_CR25","doi-asserted-by":"crossref","unstructured":"Price, T.W., Marwan, S., Winters, M., Williams, J.J.: An evaluation of data-driven programming hints in a classroom setting. In: AIED (2), LNCS, vol. 12164, pp. 246\u2013251. Springer (2020)","DOI":"10.1007\/978-3-030-52240-7_45"},{"key":"8_CR26","unstructured":"Rivers, K.: Automated Data-Driven Hint Generation for Learning Programming. Ph.D. thesis, Carnegie Mellon University, USA (2017)"},{"key":"8_CR27","doi-asserted-by":"crossref","unstructured":"Rivers, K., Koedinger, K.R.: A canonicalizing model for building programming tutors. In: ITS, LNCS, vol.\u00a07315, pp. 591\u2013593. Springer (2012)","DOI":"10.1007\/978-3-642-30950-2_80"},{"issue":"1","key":"8_CR28","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/s40593-015-0070-z","volume":"27","author":"K Rivers","year":"2017","unstructured":"Rivers, K., Koedinger, K.R.: Data-driven hint generation in vast solution spaces: a self-improving python programming tutor. Int. J. Artif. Intell. Educ. 27(1), 37\u201364 (2017)","journal-title":"Int. J. Artif. Intell. Educ."},{"key":"8_CR29","unstructured":"Sarkar, A., Negreanu, C., Zorn, B., Ragavan, S.S., P\u00f6litz, C., Gordon, A.D.: What is it like to program with artificial intelligence? In: PPIG, pp. 127\u2013153. Psychology of Programming Interest Group (2022)"},{"key":"8_CR30","doi-asserted-by":"crossref","unstructured":"Wang, K., Sullivan, A., Khurshid, S.: Automated model repair for Alloy. In: ASE, pp. 577\u2013588. ACM (2018)","DOI":"10.1145\/3238147.3238162"},{"key":"8_CR31","doi-asserted-by":"crossref","unstructured":"Zheng, G., et al.: ATR: template-based repair for Alloy specifications. In: ISSTA, pp. 666\u2013677. ACM (2022)","DOI":"10.1145\/3533767.3534369"}],"container-title":["Lecture Notes in Computer Science","Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-71177-0_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,28]],"date-time":"2024-11-28T01:09:56Z","timestamp":1732756196000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-71177-0_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,9,13]]},"ISBN":["9783031711763","9783031711770"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-71177-0_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024,9,13]]},"assertion":[{"value":"13 September 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"value":"FM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Milan","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 September 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 September 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fm2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.fm24.polimi.it\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}