Date and Location
9th International Conference on Rigorous State-Based Methods
May 20th to June 2nd, 2023
Nancy, France
Date and time TBD
Topic and Goal
Due to the simplicity and flexibility of the language and intuitive and automatic feedback provided by its analyzer, Alloy is often taught in introductory formal methods courses. However, the classic standalone Alloy Analyzer suffers from some limitations that hinder its usage in the classroom, namely i) the lack of a straightforward mechanism to share simple Alloy models, instances and associated themes, a process that becomes cumbersome in large classes where students require feedback or have to submit exercise resolutions for evaluation; and ii) the absence of some automated assessment functionality or online judge system for students to autonomously solve exercises and receive automatic feedback regarding the correctness of their resolutions.
The Alloy4Fun platform was developed precisely to address these issues. Alloy4Fun allows users to edit and execute Alloy 6 models online, providing a minimalistic customizable instance visualizer. Both models and instances can be easily shared through permalinks. Moreover, the platform provides support for simple specification challenges in the form of duels where students attempt to discover a secret constraint specified by the instructors. When solving these challenges, students are supported by a hint system to nudge them in the right direction when stuck. Alloy4Fun collects anonymized information about the student submissions and interactions, so that instructors can measure the progress of the students on the shared challenges and identify potential learning bottlenecks.
The goal of this 2 hour tutorial is to introduce participants to Alloy4Fun and its functionalities, and to show how it can be used to create and share specification challenges to be used in classes. The tutors of this tutorial have been teaching Alloy for several years at the graduate level aided by Alloy4Fun, and will share their experience on which kind of exercises are best suited to deploy in Alloy4Fun, as well as the best strategies to provide useful feedback to the students. Moreover, the tutorial will show how to explore the data collected by Alloy4Fun to analyze how students approach each shared challenge, and how successful they are.
After the tutorial, participants will be able to create challenges in Alloy4Fun, deploy them in their classes, and analyze the collected data. Due to the abstract nature of Alloy, we believe it is suitable not only in formal methods courses, but also for those teaching discrete mathematics or logic.
Prerequisites
Basic knowledge of Alloy is helpful, although it is not required to understand the functionalities of Alloy4Fun, the proposed teaching approach, nor the simple challenges that will be presented. No tool needs to be downloaded or installed since only the Alloy4Fun platform will be used.
Agenda
- Very brief introduction to Alloy 6 language (15min)
- Structure, relational logic, temporal logic, commands
- Introduction to the Alloy4Fun platform (15min)
- Editor, execution, visualizer, themes
- Model and instance sharing mechanisms
- Creation of challenges in Alloy4Fun (60min)
- Model secrets and public links
- Student challenges as secrets
- Feedback to students, counter-examples and hints
- Typical classes of challenges
- Lessons learned
- Exploring tutor feedback (30min)
- Data model and derivation trees
- Metrics, statistics, graph view
- Offline advanced analyses
Tutors
- Alcino Cunha is an Assistant Professor at the University of Minho and a researcher at the High-Assurance Software Laboratory of INESC TEC, Portugal. He has been teaching Alloy at the graduate level since 2007, supported by Alloy4Fun since 2019. He actively researches on Alloy-related topics, and was one of the proponents of Alloy 6 and Alloy4Fun.
- Nuno Macedo is an Assistant Professor at the Faculty of Engineering of the University of Porto and a researcher at the High-Assurance Software Laboratory of INESC TEC, Portugal. He has been teaching Alloy at the graduate level since 2015, supported by Alloy4Fun since 2019. He actively researches on Alloy-related topics, and was one of the proponents and maintainers of Alloy 6 and Alloy4Fun.