1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
<!DOCTYPE html>
<html lang="en">
<head>
<meta charset="utf-8">
<meta name="viewport" content="width=device-width, initial-scale=1">
<title>Forge: A Tool and Language for Teaching Formal Methods</title>
<meta name="author" content="Tim Nelson, Ben Greenman, Siddhartha Prasad, Tristan Dyer, Ethan Bove, Qianfan Chen, Charles Cutting, Thomas Del Vecchio, Sidney LeVine, Julianne Rudner, Ben Ryjikov, Alexander Varga, Andrew Wagner, Luke West, Shriram Krishnamurthi">
<meta name="description" content="Forge is a tool for teaching formal methods gradually, based on Alloy. OOPSLA 2024.">
<link rel="canonical" href="https://doi.org/10.1145/3649833">
<style>
:root {
  --ink: #16161a;
  --muted: #5a5a66;
  --rule: #d8d8e0;
  --link: #7c1773;
  --accent: #004f91;
  --bg: #fdfdfb;
  --code-bg: #f4f4f0;
}
@media (prefers-color-scheme: dark) {
  :root {
    --ink: #e6e6e6; --muted: #a0a0ac; --rule: #33333c;
    --link: #d79ad2; --accent: #8ab8e6; --bg: #16161a; --code-bg: #22222a;
  }
}
* { box-sizing: border-box; }
html { font-size: 17px; }
body {
  margin: 0 auto; padding: 2.5rem 1.25rem 6rem; max-width: 42rem;
  background: var(--bg); color: var(--ink);
  font-family: "Linux Libertine", Libertinus Serif, Palatino, Georgia, serif;
  line-height: 1.6; text-rendering: optimizeLegibility;
}
a { color: var(--link); }
a:hover { text-decoration-thickness: 2px; }
h1 { font-size: 1.9rem; line-height: 1.25; margin: 0 0 1rem; font-weight: 600; }
h2, h3, h4 {
  font-family: "Linux Biolinum", Optima, "Segoe UI", system-ui, sans-serif;
  line-height: 1.3; margin: 2.4rem 0 .6rem; font-weight: 600;
}
h2 { font-size: 1.35rem; border-bottom: 1px solid var(--rule); padding-bottom: .3rem; }
h3 { font-size: 1.12rem; }
h4 { font-size: 1rem; display: inline; margin-right: .4rem; }
h4 + p { display: inline; }
.num { color: var(--muted); font-variant-numeric: tabular-nums; margin-right: .35em; }
p { margin: 0 0 .85rem; hyphens: auto; }
.venue { color: var(--muted); font-size: .82rem; margin-bottom: .6rem; }
.paper-head { border-bottom: 2px solid var(--rule); padding-bottom: 1.2rem; }
ol.authors { list-style: none; margin: 0; padding: 0;
  display: flex; flex-wrap: wrap; gap: .15rem 1.1rem; font-size: .92rem; }
ol.authors li { white-space: nowrap; }
.aff { color: var(--muted); font-size: .8rem; margin-left: .35em; }
.abstract { margin: 1.8rem 0; font-size: .97rem; }
.abstract h2 { font-size: .82rem; text-transform: uppercase;
  letter-spacing: .09em; border: 0; color: var(--muted); margin: 0 0 .5rem; }
.ccs, .kw { font-size: .85rem; color: var(--muted); }
code {
  font-family: Inconsolata, "SF Mono", ui-monospace, Menlo, monospace;
  font-size: .88em; background: var(--code-bg); padding: .08em .3em;
  border-radius: 3px; word-break: break-word;
}
pre {
  background: var(--code-bg); border: 1px solid var(--rule); border-radius: 5px;
  padding: .85rem 1rem; overflow-x: auto; margin: 0; line-height: 1.45;
}
pre code { background: none; padding: 0; font-size: .84rem; white-space: pre; }
/* Only images are centred.  Setting text-align on the figure itself would
   be inherited by <pre>, centring every line of a code listing. */
figure { margin: 1.8rem 0; }
figure .figbody { text-align: center; }
figure pre { text-align: left; }
figure img { max-width: 100%; height: auto; border: 1px solid var(--rule);
  border-radius: 4px; background: #fff; display: block; margin: 0 auto; }
/* Figures that hold several images sit side by side until the screen is
   too narrow, then stack. */
.figrow { display: flex; flex-wrap: wrap; gap: .75rem;
  justify-content: center; align-items: flex-end; }
.figrow .zoom { flex: 0 1 auto; max-width: 100%; }
/* A figure whose two halves are different kinds of thing: a table beside a
   stack of screenshots (fig. 11).  They sit side by side while there is
   room and stack when there is not. */
.figsplit { display: flex; flex-wrap: wrap; gap: 1.2rem;
  align-items: flex-start; justify-content: center; }
.figsplit .figtable { flex: 1 1 20rem; min-width: 16rem; }
.figsplit .figtable table { margin: 0; font-size: .82rem; }
.figsplit .figtable td, .figsplit .figtable th { padding: .18rem .4rem; }
.figsplit .figshots { flex: 1 1 16rem; display: flex;
  flex-direction: column; gap: .7rem; align-items: center; }
.figsplit .subfig { margin: 0; }
.subfig figcaption { text-align: center; font-size: .8rem;
  margin-top: .35rem; }
button.zoom { padding: 0; border: 0; background: none; cursor: zoom-in;
  display: inline-block; max-width: 100%; }
button.zoom:focus-visible img { outline: 3px solid var(--accent);
  outline-offset: 2px; }
button.zoom:hover img { border-color: var(--accent); }
dialog.lightbox { border: 0; padding: 0; background: none; max-width: 100vw;
  max-height: 100vh; width: 100%; height: 100%; overflow: auto; }
dialog.lightbox::backdrop { background: rgba(0, 0, 0, .82); }
dialog.lightbox img { display: block; margin: auto; background: #fff;
  border-radius: 4px; max-width: 96vw; }
/* The images are ~3x the size the PDF showed them at, so enlarging is
   worthwhile; allow panning when the natural size exceeds the viewport. */
dialog.lightbox .wrap { min-height: 100%; display: grid; place-items: center;
  padding: 1rem; }
dialog.lightbox .close { position: fixed; top: .75rem; right: 1rem;
  font: inherit; font-size: 1.1rem; line-height: 1; color: #fff;
  background: rgba(0, 0, 0, .55); border: 1px solid rgba(255, 255, 255, .4);
  border-radius: 4px; padding: .4rem .6rem; cursor: pointer; }
figcaption { font-family: "Linux Biolinum", Optima, system-ui, sans-serif;
  font-size: .85rem; color: var(--muted); text-align: left;
  margin-top: .6rem; line-height: 1.45; }
table { border-collapse: collapse; width: 100%; font-size: .88rem;
  margin: 1rem 0; }
th, td { border-bottom: 1px solid var(--rule); padding: .4rem .5rem;
  text-align: left; }
thead th { border-bottom: 2px solid var(--ink); }
td.yes { color: #2e7d32; font-weight: 700; }
td.no { color: #b03030; }
ul, ol { padding-left: 1.4rem; margin: 0 0 .9rem; }
/* Description lists: the term stays a run-in label, as in the paper, but
   the term/definition relationship is now in the markup. */
dl { margin: 0 0 .9rem; }
dl dt { font-weight: 600; float: left; clear: left; margin-right: .4em; }
dl dt::after { content: "."; }
dl dd { margin: 0 0 .55rem 1.4rem; }
@media (max-width: 34rem) {
  dl dt { float: none; margin-bottom: .15rem; }
  dl dd { margin-left: 1rem; }
}
p.runin { font-weight: 600; margin-bottom: .3rem; }
li { margin-bottom: .35rem; }
abbr { font-variant: small-caps; text-transform: lowercase;
  letter-spacing: .02em; text-decoration: none; }
/* Sidenotes: the note sits in the right margin, level with the mark that
   references it.  The <aside> follows the mark in document order, so with
   CSS off it still reads as a note in the right place. */
.fnref { text-decoration: none; }
.fnref sup { font-size: .72em; padding: 0 .1em; }
.sidenote {
  display: block;
  float: right; clear: right;
  width: 15rem; margin: .2rem -17rem .8rem 1rem;
  font-size: .78rem; line-height: 1.45; color: var(--muted);
  text-align: left; text-indent: 0;
}
.sidenote .fnnum { font-weight: 700; color: var(--ink); margin-right: .25em; }
.sidenote code { font-size: .95em; }
/* Not enough room beside the text: fall back to an indented inline note. */
@media (max-width: 78rem) {
  .sidenote {
    float: none; width: auto; margin: .7rem 0;
    padding: .55rem .8rem; border-left: 3px solid var(--rule);
    background: var(--code-bg); display: block;
  }
}
.backrefs { margin-left: .35em; white-space: nowrap; }
.backrefs a { text-decoration: none; font-size: .9em; opacity: .65; }
.backrefs a:hover { opacity: 1; }
.footnotes, .references { margin-top: 3rem; font-size: .87rem; }
.footnotes li, .references li { margin-bottom: .55rem; }
.references a { word-break: break-all; }
.toc { margin: 2rem 0; font-size: .9rem; }
.toc ol { list-style: none; padding-left: 0; }
.toc ol ol { padding-left: 1.2rem; }
.toc a { text-decoration: none; color: var(--accent); }
.toc a:hover { text-decoration: underline; }
.srconly { position: absolute; width: 1px; height: 1px; overflow: hidden;
  clip: rect(0 0 0 0); }
.provenance {
  font-size: .82rem; line-height: 1.5; color: var(--muted);
  border: 1px solid var(--rule); border-left: 4px solid var(--accent);
  border-radius: 4px; padding: .7rem .9rem; margin: 0 0 2rem;
  background: var(--code-bg);
}
.provenance a { color: var(--accent); }
.license { margin-top: 3rem; padding-top: 1rem; border-top: 1px solid var(--rule);
  font-size: .8rem; color: var(--muted); }
</style>
</head>
<body>
<p class="provenance">
  This is an <b>unofficial HTML rendering</b> of a paper published at OOPSLA
  2024, reproduced under its
  <a href="https://creativecommons.org/licenses/by/4.0/">CC&nbsp;BY&nbsp;4.0</a>
  licence. It is not published by, or endorsed by, the authors or the ACM.
  The authoritative version is the
  <a href="https://cs.brown.edu/people/sk/Publications/Papers/Published/ngp----forge/paper.pdf">original PDF</a> (<a href="https://doi.org/10.1145/3649833">https://doi.org/10.1145/3649833</a>);
  quote from that, not from this page.
  <!-- data-web-only marks content that ./make-epub strips: inside the EPUB
       this would link to a missing file and describe the file being read. -->
  <span data-web-only>This rendering is also available as an
  <a href="forge-paper.epub" type="application/epub+zip">EPUB</a> for
  e&#8209;readers.</span>
</p>

<header class="paper-head">
  <p class="venue">Proc. ACM Program. Lang. <b>8</b>, OOPSLA1, Article 116
     (April 2024) &middot; 29 pages</p>
  <h1>Forge: A Tool and Language for Teaching Formal Methods</h1>
  <ol class="authors">
    <li>Tim Nelson<span class="aff">Brown University, USA</span></li>
    <li>Ben Greenman<span class="aff">University of Utah, USA</span></li>
    <li>Siddhartha Prasad<span class="aff">Brown University, USA</span></li>
    <li>Tristan Dyer<span class="aff">Stashpad, USA</span></li>
    <li>Ethan Bove<span class="aff">Brown University, USA</span></li>
    <li>Qianfan Chen<span class="aff">Brown University, USA</span></li>
    <li>Charles Cutting<span class="aff">Brown University, USA</span></li>
    <li>Thomas Del Vecchio<span class="aff">Brown University, USA</span></li>
    <li>Sidney LeVine<span class="aff">Brown University, USA</span></li>
    <li>Julianne Rudner<span class="aff">Brown University, USA</span></li>
    <li>Ben Ryjikov<span class="aff">Brown University, USA</span></li>
    <li>Alexander Varga<span class="aff">Brown University, USA</span></li>
    <li>Andrew Wagner<span class="aff">Northeastern University, USA</span></li>
    <li>Luke West<span class="aff">Brown University, USA</span></li>
    <li>Shriram Krishnamurthi<span class="aff">Brown University, USA</span></li>
  </ol>
</header>

<section class="abstract" aria-label="Abstract">
  <h2>Abstract</h2>
  <p>This paper presents the design of Forge, a tool for teaching formal methods gradually. Forge is based on the widely-used Alloy language and analysis tool, but contains numerous improvements based on more than a decade of experience teaching Alloy to students. Although our focus has been on the classroom, many of the ideas in Forge likely also apply to training in industry.</p>
<p>Forge offers a progression of languages that improve the learning experience by only gradually increasing in expressive power. Forge supports custom visualization of its outputs, enabling the use of widely-understood domain-specific representations. Finally, Forge provides a variety of testing features to ease the transition from programming to formal modeling. We present the motivation for and design of these aspects of Forge, and then provide a substantial evaluation based on multiple years of classroom use.</p>
  <p class="ccs"><b>CCS Concepts:</b> • Software and its engineering → Semantics; Constraints; Functional languages.</p>
  <p class="kw"><b>Keywords:</b> lightweight formal-methods, formal-methods education, language levels</p>
</section>

<nav class="toc" aria-label="Table of contents"><h2>Contents</h2>
<ol>
<li><a href="#sec1">1 Introduction</a>
</li>
<li><a href="#sec2">2 Background: Teaching FM Gradually</a>
</li>
<li><a href="#sec3">3 A Progression of Languages</a>
<ol>
<li><a href="#sec3.1">3.1 A Critique of Alloy’s Language</a></li>
<li><a href="#sec3.2">3.2 Language Levels</a></li>
</ol>
</li>
<li><a href="#sec4">4 Custom Visualization</a>
<ol>
<li><a href="#sec4.1">4.1 Example: Crypto Protocols</a></li>
<li><a href="#sec4.2">4.2 Example: River Crossing</a></li>
<li><a href="#sec4.3">4.3 Example: Network Reachability</a></li>
</ol>
</li>
<li><a href="#sec5">5 Testing: From Rough Ideas to Reliable Models</a>
<ol>
<li><a href="#sec5.1">5.1 Alloy Critique: Testing</a></li>
<li><a href="#sec5.2">5.2 Design of Testing in Forge</a></li>
</ol>
</li>
<li><a href="#sec6">6 Architecture and Implementation</a>
</li>
<li><a href="#sec7">7 Evaluation</a>
<ol>
<li><a href="#sec7.1">7.1 Evaluation: Language Levels</a></li>
<li><a href="#sec7.2">7.2 Evaluation: Custom Visualization</a></li>
<li><a href="#sec7.3">7.3 Formative Evaluation: Testing</a></li>
</ol>
</li>
<li><a href="#sec8">8 Related Work</a>
</li>
<li><a href="#sec9">9 Discussion</a>
</li>
</ol></nav>

<p><strong>ACM Reference Format:</strong> Tim Nelson, Ben Greenman, Siddhartha Prasad, Tristan Dyer, Ethan Bove, Qianfan Chen, Charles Cutting, Thomas Del Vecchio, Sidney LeVine, Julianne Rudner, Ben Ryjikov, Alexander Varga, Andrew Wagner, Luke West, and Shriram Krishnamurthi. 2024. Forge: A Tool and Language for Teaching Formal Methods. <em>Proc. ACM</em> <em>Program. Lang.</em> 8, OOPSLA1, Article 116 (April 2024), 29 pages. <a href="https://doi.org/10.1145/3649833">https://doi.org/10.1145/3649833</a></p>
<h2 id="sec1"><span class="num">1</span> Introduction</h2>
<p>The growing applicability of formal methods (<span class="sc">fm</span>) demands that we create curricula and tools that serve broad audiences, not only those who were already predisposed to learning the topic. Yet, “<span class="sc">fm</span>” comprises many techniques and tools: proof assistants, dependently-typed languages, property-based testing, model checking, SMT solvers, and more (e.g., <a href="#ref12" id="cite2" role="doc-biblioref">Brady</a> [<a href="#ref12" id="cite3" role="doc-biblioref">2013</a>]; <a href="#ref16" id="cite4" role="doc-biblioref">Claessen and Hughes</a> [<a href="#ref16" id="cite5" role="doc-biblioref">2000</a>]; <a href="#ref18" id="cite6" role="doc-biblioref">de Moura and Bjørner</a> [<a href="#ref18" id="cite7" role="doc-biblioref">2008</a>]; <a href="#ref36" id="cite8" role="doc-biblioref">Holzmann</a> [<a href="#ref36" id="cite9" role="doc-biblioref">2003</a>]; <a href="#ref43" id="cite10" role="doc-biblioref">Leino</a> [<a href="#ref43" id="cite11" role="doc-biblioref">2010</a>]; <a href="#ref52" id="cite12" role="doc-biblioref">Nipkow et al.</a> [<a href="#ref52" id="cite13" role="doc-biblioref">2002</a>])—not all of which are good fits for students without a formal bent. In this paper we adopt a specific class of <span class="sc">fm</span> that we believe is well-suited to broad computer-science education, and then describe student-friendly tools that implement it.</p>
<p>Our inspiration is Alloy [<a href="#ref39" id="cite14" role="doc-biblioref">Jackson 2012</a>]. Alloy embodies the <em>lightweight</em> <span class="sc">fm</span> philosophy exposited by <a href="#ref41" id="cite15" role="doc-biblioref">Jackson and Wing</a> [<a href="#ref41" id="cite16" role="doc-biblioref">1996</a>], and relative to many other <span class="sc">fm</span> tools, it offers numerous advantages for introducing <span class="sc">fm</span>:</p>
<ul>
  <li>It provides a rich, relational, language. Its relational nature makes it suitable for expressing object relationships [<a href="#ref38" id="cite17" role="doc-biblioref">Jackson 2002</a>; <a href="#ref58" id="cite18" role="doc-biblioref">Spivey 1992</a>], which reflect a wide variety of systems encountered in daily life. Thus, Alloy allows students to explore their intrinsic interests via formal modeling—both within and outside of computing.</li>
  <li>It has a syntax reminiscent of programming languages like Java, meaning that students can import some amount of object-oriented experience when starting with Alloy—learning the tool’s more powerful features as they progress.</li>
  <li>It offers push-button automation. Therefore, it feels familiar to students coming from a background of <span class="sc">ide</span>s. Just as students might click “run” in an <span class="sc">ide</span> to execute their program, they can click “run” in Alloy to generate satisfying instances of their model.</li>
  <li>It supports multiple modes of use. In the presence of properties, it behaves as a bounded model checker [<a href="#ref10" id="cite19" role="doc-biblioref">Biere et al. 1999</a>]. However, in the absence of properties, students can still “run” their model to explore concrete instances, which may trigger a deeper understanding (including of undesired behaviors). This relates to the surprise-explain-reward model [<a href="#ref64" id="cite20" role="doc-biblioref">Wilson et al. 2003</a>] of cognition used in other tools for aiding correctness (e.g., [<a href="#ref42" id="cite22" role="doc-biblioref">Jernigan et al. 2017</a>]). This modality stands in contrast to many other verification tools, such as many model checkers, which are inert in the absence of properties.</li>
  <li>It gives an automatic <em>visualization of instances</em>. When students view an instance, Alloy’s visualizer presents it as a labeled directed graph, which is often a vast improvement over raw textual formats. If students prefer a tabular view, Alloy offers that as well.</li>
</ul>
<p>Consequently, Alloy is popular and widely-used in both education and practice [<a href="#ref2" id="cite23" role="doc-biblioref">alloytools.org 2023a</a>,<a href="#ref3" id="cite25" role="doc-biblioref">b</a>,<a href="#ref4" id="cite26" role="doc-biblioref">c</a>; <a href="#ref40" id="cite27" role="doc-biblioref">Jackson 2019</a>]. However, based on several years of teaching with Alloy, we have found critical weaknesses in it for the purposes of our pedagogy:</p>
<ul>
  <li>Alloy’s sophisticated language and clever syntax contain pitfalls for students.</li>
  <li>Alloy’s visualizer can produce unhelpful, confusing, or outright misleading output.</li>
  <li>Alloy’s support for testing is limited, which hinders some educational opportunities for students who have programming experience.</li>
</ul>
<p>In response, we have built a system named Forge,<a class="fnref" id="fnref1" href="#fn1" role="doc-noteref"><sup>1</sup></a><span class="sidenote" id="fn1" role="note"><span class="fnnum">1</span> The name is of course intended as a tribute to Alloy. It should not be confused with the Alloy-based but unrelated, defunct Forge tool [<a href="#ref19" id="cite1" role="doc-biblioref">Dennis et al. 2006</a>].</span> designed to be a pedagogic variant of Alloy. Like Alloy, Forge is a language and a tool, and it draws heavily on Alloy’s syntax, semantics, and infrastructure. Forge has three critical innovations:</p>
<dl>
  <dt>Language Levels</dt>
  <dd>Forge supports a <em>progression</em> of sub-languages that build on each other and elide unnecessary complexity (section <a href="#sec3">3</a>). These sub-languages are not merely optional fragments of one overall language, but provide their own <em>epistemic closure</em> [<a href="#ref31" id="cite28" role="doc-biblioref">Findler et al. 2002</a>] by, e.g., ensuring that error messages are given in terms of the current sub-language.</dd>
  <dt>Custom Visualization</dt>
  <dd>Forge broadens Alloy’s default visualizations, building atop a Web-based visualizer [<a href="#ref24" id="cite30" role="doc-biblioref">Dyer 2020</a>] to include <em>custom visualizations</em> (section <a href="#sec4">4</a>). We have built several visualizations to further epistemic closure for homework problems, and students have built their own visualizations for domains of their choosing (examples in section <a href="#sec7">7</a>).</dd>
  <dt>Testing</dt>
  <dd>Forge adds linguistic support for testing throughout model development (section <a href="#sec5">5</a>).</dd>
</dl>
<p>In addition, Forge is built atop the Racket platform [<a href="#ref29" id="cite31" role="doc-biblioref">Felleisen et al. 2018</a>], enabling additional (as yet pedagogically untested) benefits such as domain-specific modeling languages (section <a href="#sec9">9</a>).</p>
<p>While our focus in this paper is on teaching <span class="sc">fm</span> at the tertiary education level, we conjecture that all these elements would benefit industrial users as well, especially trainees. Indeed, one of our main examples for custom visualization is from a more expert setting (section <a href="#sec4.3">4.3</a>).</p>
<p><em>Outline.</em> After a short background on our <span class="sc">fm</span> pedagogy (section <a href="#sec2">2</a>), this paper presents the design of language levels (section <a href="#sec3">3</a>), custom visualization (section <a href="#sec4">4</a>), and testing tools (section <a href="#sec5">5</a>) in Forge. This tour of Forge concludes with a brief discussion of its architecture and implementation (section <a href="#sec6">6</a>). The second half of the paper contains a substantial evaluation of Forge, both quantitative and qualitative, based on multiple years of using Forge in the classroom (section <a href="#sec7">7</a>). The paper concludes with related work (section <a href="#sec8">8</a>) and high-level reflections (section <a href="#sec9">9</a>).</p>
<p>Forge is Open Source. The project is available from: <a href="https://forge-fm.org/">https://forge-fm.org/</a> This paper also comes with an artifact that includes the models and visualizations we reference herein, along with copies of Forge and its documentation [<a href="#ref49" id="cite32" role="doc-biblioref">Nelson et al. 2024</a>].</p>
<h2 id="sec2"><span class="num">2</span> Background: Teaching FM Gradually</h2>
<p>There are many potential ways to teach <span class="sc">fm</span>. We espouse a <em>gradual</em> approach, which starts by meeting students where they are conceptually. Most notably, this includes the many students who are deeply uninterested in formalism, but are becoming experts in other fields such as distributed systems or security. Our goal is not to convert these students into <span class="sc">fm</span> fans, but rather to equip them with basic training before they go on to build tomorrow’s digital infrastructure. We want all students to learn how to apply formal approaches to their own areas of interest and expertise.</p>
<p>Gradual <span class="sc">fm</span> comprises four core ideas:</p>
<ul>
  <li><em>Teach with tools.</em> Software tools lower the barrier to entry (since the tool can actively guide the student, unlike paper and pencil) and provide a familiar “programming”-esque environment in which to work. If the tool also provides rapid feedback, so much the better.</li>
  <li><em>Embrace lightweight</em> <span class="sc">fm</span><em>.</em> Drawing inspiration from <a href="#ref41" id="cite33" role="doc-biblioref">Jackson and Wing</a> [<a href="#ref41" id="cite34" role="doc-biblioref">1996</a>], we use languages with limited expressive power to enable quick, low-cost formal analysis. As a result, we focus on modeling partial systems, precisely stating properties, and revealing bugs, rather than on proving that no bugs exist.</li>
  <li><em>Be systems-oriented.</em> While some students get excited modeling a programming language or other abstract topics, we find it is far more common for students to embrace concrete goals such as modeling a distributed hash table or a search algorithm. Gradual <span class="sc">fm</span> focuses more on the latter, systems-oriented topics.</li>
  <li><em>Leverage programming intuitions.</em> We assume that students will have experience with programming and unit testing but perhaps no other common background—not even a course in discrete math. This setting is especially suited to modeling with objects and functions. Likewise, testing strategies that students have seen should be used to teach (e.g., using unit testing to understand satisfiability), not just be disparaged for their incompleteness.</li>
</ul>
<p>For all the reasons mentioned in section <a href="#sec1">1</a>—including its accessible syntax, push-button automation, visualization, etc.—Alloy is a good starting point for implementing a gradual <span class="sc">fm</span> pedagogy.</p>
<p><em>Experience context:</em> The experiences reported in this paper were run in the context of such a gradual course on <span class="sc">fm</span> that we have taught for a decade. The course, Logic for Systems (<span class="sc">l4s</span>), began developing a pedagogy in 2013 and migrated from Alloy to an early version of Forge in 2019. Later years extended Forge with language levels (2021), temporal operators (2021), and tools for custom visualization (2022).</p>
<p><span class="sc">l4s</span> is offered in the computer-science department at Brown, a selective private research university. The only prerequisite for enrollment is an introductory programming course. Our students came in with a variety of coursework experience. Some had taken only a one-semester accelerated introductory course using Pyret because they had prior programming experience. Some had completed a year-long introductory sequence using Java and one of Pyret, Racket, or ReasonML. The majority were upper-level students with additional experience, and a few were graduate students. Many students had some industrial internship experience as well. However, virtually none of them had prior formal-methods coursework. We suspect they also got no exposure to <span class="sc">fm</span> in industry. There were 92 students enrolled in 2022 and 64 students in 2023.</p>
<h2 id="sec3"><span class="num">3</span> A Progression of Languages</h2>
<p>Alloy includes a powerful language, but, when it comes to teaching, one full-featured language is less ideal than a step-by-step progression of languages. We start with a critique of Alloy (section <a href="#sec3.1">3.1</a>); this motivates the languages in Forge (section <a href="#sec3.2">3.2</a>). We defer evaluation to section 7.</p>
<h3 id="sec3.1"><span class="num">3.1</span> A Critique of Alloy’s Language</h3>
<p>Over the years, we have observed several issues that Alloy presents to learners. We stress that, in general, we find Alloy’s language very effective for software modeling; we want programmers to learn how to use it. Rather, our observations are about identifying ways to improve the language <em>with pedagogy in mind</em>.</p>
<h4 id="sec3.1.1"><span class="num">3.1.1</span> Critique: Functions vs. Relations.</h4>
<p>While on the surface Alloy has a Java-esque syntax, its semantics is based on relations. Alloy makes clever use of relational operators to support an apparently object-oriented style of modeling. For example, Alloy’s join operator is written as <code>.</code> (dot) and thus <em>looks</em> like a field access, as in <code>p.father</code>. Early on this pun gets students comfortable working with Alloy. However, at some point, students realize that the semantics is not what they expected based on syntactic recall (which seems to happen no matter what we teach in class): “backwards accesses” such as <code>father.p</code> are perfectly sensible joins.</p>
<p>Another issue arises from the fact that all Alloy expressions evaluate to sets. In a model of family trees, we might write that there exists some person whose father is their only friend:</p>
<pre><code><b>some</b> p: Person | p.friends = p.father</code></pre>
<p>Since both <code>p.friends</code> and <code>p.father</code> are expressions, and expressions evaluate to sets, the equality makes sense semantically. But to a student whose prior context is a language like Java, where the type <code>Person</code> is different from <code>Set&lt;Person&gt;</code>, this leads to confusion: shouldn’t the formula produce a type error, since <code>p.father</code> is always a person, not a set <em>of</em> persons?</p>
<h4 id="sec3.1.2"><span class="num">3.1.2</span> Critique: Syntactic Sugar.</h4>
<p>Alloy’s language also contains syntactic choices that are convenient to expert modelers but problematic for students. We list two subtle examples below.</p>
<p><strong>Non-compositionality:</strong> The following shorthand constraint, taken from <a href="#ref39" id="cite35" role="doc-biblioref">Jackson</a> [<a href="#ref39" id="cite36" role="doc-biblioref">2012</a>, ch. 6], says that the <code>keys</code> relation is a partial function between the set <code>Key</code> and the set <code>Room</code>:</p>
<pre><code>keys <b>in</b> Room <b>lone</b> -&gt; Key</code></pre>
<p>If a student tries to experiment with the subexpression <code>Room lone -&gt; Key</code> to understand the impact of <code>lone</code>, they will find no impact; the subexpression is equivalent to <code>Room -&gt; Key</code>. This is because the meaning of <code>lone</code> applies to the <code>in</code> operator—even though <code>lone</code> appears syntactically within the cross-product (<code>-&gt;</code>) expression.</p>
<p><strong>Quantification:</strong> Alongside the standard first-order <code>all</code> (∀) and <code>some</code> (∃) quantifiers, Alloy provides <code>no</code> and <code>one</code> as well, which are just shorthand for more complex formulas. However, some properties of basic quantifiers do not apply to these advanced ones. For instance, <code>some</code> distributes over disjunction but <code>one</code> does not. Alloy also allows multiple variables to be grouped under the same quantifier, but advanced quantifiers can behave unexpectedly:</p>
<pre><code><b>no</b> x, y: A | . . .    is <i>not</i> equivalent to    <b>no</b> x: A | <b>no</b> y: A | . . .</code></pre>
<p><em>“there is no pair</em> (𝑥, 𝑦) <em>such that...”</em> ≠ <em>“there is no</em> 𝑥 <em>such that there is no</em> 𝑦 <em>such that...”</em></p>
<h3 id="sec3.2"><span class="num">3.2</span> Language Levels</h3>
<p>Problems like these present us with a quandary: for experts, or at least for compatibility, we need the full power of the language. But for learners, we want to begin with a simple language and gradually introduce useful features. Textbooks often follow exactly such a progression, but tools do not always mirror it. Therefore, students can either be tripped up by richer semantics than they expected, or can stumble on keywords (e.g., from documentation, StackOverflow, or even generative AI tools) that do not do what they wanted. These issues with the professional-grade language lead to student frustration, adding to the high cognitive load imposed by learning about specification, and often result in erroneous conclusions, which are dangerous in verification.</p>
<p>A solution proposed by multiple teams over the years is to use <em>language levels</em> [<a href="#ref23" id="cite37" role="doc-biblioref">du Boulay et al. 1999</a>; <a href="#ref31" id="cite39" role="doc-biblioref">Findler et al. 2002</a>; <a href="#ref35" id="cite40" role="doc-biblioref">Holt and Wortman 1974</a>]. That is, instead of just a single language, present a <em>progression of sub-languages</em> that grows with student instruction and accomplishment. This process has been implemented for the book <em>How to Design Programs</em> [<a href="#ref28" id="cite41" role="doc-biblioref">Felleisen et al. 2001</a>] in the DrRacket <span class="sc">ide</span>. Other textbooks and languages, e.g., Grace [<a href="#ref37" id="cite42" role="doc-biblioref">Homer et al. 2014</a>], have also exploited this idea.</p>
<p>Readers familiar with Alloy may be reminded of its three modes of use [<a href="#ref39" id="cite43" role="doc-biblioref">Jackson 2012</a>]: navigation, predicate calculus, and relational calculus. These correspond roughly to language levels in that they use a fragment of the full syntax, but nothing prevents students from straying outside a language boundary. For example, suppose a student is working with a family-tree model, and accidentally reverses the arguments to the dot (<code>.</code>) operator when referring to someone’s mother:</p>
<pre><code>mother.Ani = Barbara</code></pre>
<p>An early language level, in which dot represents field access, should report an error—even though this “error” is a perfectly valid and well-typed expression in the full Alloy language. Moreover, if a student makes a type error, such as asking for the <code>population</code> (a property of cities) of a person:</p>
<pre><code>Ani.population</code></pre>
<p>An early language level should not give the standard Alloy message: “the join operation here always yields an empty set” [<a href="#ref26" id="cite44" role="doc-biblioref">Edwards et al. 2004</a>]. This is a reasonable error only if the student knows what a join is! Instead, the first Forge language says “sig does not have such a field.” The key is that all feedback—such as error messages—must use only concepts that have been introduced so far [<a href="#ref31" id="cite45" role="doc-biblioref">Findler et al. 2002</a>], otherwise the epistemic closure of the language is lost.</p>
<p>Forge provides students with three separate language levels. Each closely resembles the Alloy language, but with targeted restrictions and improvements:</p>
<ol>
  <li><strong>Froglet</strong> is a restriction of the relational Alloy language to <em>partial functions</em>, rather than relations. Sets and most relational operators are absent; the <code>.</code> operator behaves like field access. Top-level expressions evaluate to singletons. Error messages are in terms of objects, fields, etc. Froglet also provides a <code>reachable</code> helper predicate that can express basic reachability constraints without the transitive-closure operator. Lacking recourse to relational operators, students must use explicit quantification—reinforcing their facility with basic concepts.</li>
  <li><strong>Relational Forge</strong> adds sets and relational operators such as union and transpose. At this point in the curriculum our students are familiar with basic concepts and are prepared to focus more deeply on the underlying relational nature of the language. This level also introduces shorthand quantifiers such as <code>one</code> and <code>no</code>. Moreover, students can now cleanly model weighted graphs and other concepts that are much easier to represent with arbitrary-arity relations than boolean-valued functions. Relations are therefore easy to motivate.</li>
  <li><strong>Temporal Forge</strong> introduces time and temporal logic operators, in the style of Alloy 6 [<a href="#ref1" id="cite46" role="doc-biblioref">alloytools.org 2023</a>; <a href="#ref45" id="cite48" role="doc-biblioref">Macedo et al. 2016</a>]. This is a tricky step because students are progressing from finite-length traces to infinite ones. Subtle issues invariably arise, such as the question of how to model a deadlock state within an infinite trace. However, the staging of languages means that students have already become familiar with relations, and can therefore focus on understanding temporal logic without additional cognitive burden.</li>
</ol>
<p>Students are told for each assignment which level to use (or, on larger projects, which levels they may choose from). As is standard in Racket languages, the language is chosen in the first line of each source file [<a href="#ref29" id="cite49" role="doc-biblioref">Felleisen et al. 2018</a>]. Thus, these rules can even be enforced in a grading system. In our experience, it does not take very long at all for students to understand language levels.</p>
<p>Table <a href="#tab1">1</a> shows a comparison of features between Forge language levels and Alloy 6. Alloy has features, such as global constraints, that no Forge language supports but that expert users (including the authors) find valuable. Figures <a href="#fig1">1</a> to 3 show one example model for each Forge level: fig. <a href="#fig1">1</a> demonstrates quantification in Froglet, fig. <a href="#fig2">2</a> uses transitive closure in Relational Forge, and fig. <a href="#fig3">3</a> specifies an increasing counter in Temporal Forge. For space, we show the most pertinent parts of each example; the full files are available in the artifact.</p>
<h2 id="sec4"><span class="num">4</span> Custom Visualization</h2>
<p>Forge integrates the Sterling visualizer [<a href="#ref24" id="cite50" role="doc-biblioref">Dyer 2020</a>]. At first glance, this simply replaces Alloy’s default visualization style with a modern Web-based interface. However, Forge also leverages Sterling’s support for <em>custom visualizations</em> to both provide domain-specific visualizations for homework problems and to enable students to create their own visualizations. Custom visualizations are written in JavaScript and can either manipulate the Sterling page directly, use the D3 data-visualization library [<a href="#ref53" id="cite51" role="doc-biblioref">Observable 2023</a>], or leverage a number of built-in quick-prototyping features. Refer to our artifact or the Forge documentation for code examples.</p>
<p>Custom visualizations are much more than pretty pictures. They serve a valuable pedagogic purpose by avoiding confusion and lowering the cognitive load to understanding. Visualizations are especially important if <span class="sc">fm</span> tools are to reach students outside of <span class="sc">fm</span>—easily-comprehensible</p>
<figure id="tab1">
  <table>
<thead><tr><th scope="col">Language feature</th><th scope="col">Froglet</th><th scope="col">Rel. Forge</th><th scope="col">Temporal Forge</th><th scope="col">Alloy 6</th></tr></thead>
<tbody>
<tr><th scope="row">Partial-function fields, <code>some</code>, <code>all</code> quantifiers</th><td class="yes" aria-label="yes">✓</td><td class="yes" aria-label="yes">✓</td><td class="yes" aria-label="yes">✓</td><td class="yes" aria-label="yes">✓</td></tr>
<tr><th scope="row">Dedicated testing constructs (<a href="#sec5">section 5</a>)</th><td class="yes" aria-label="yes">✓</td><td class="yes" aria-label="yes">✓</td><td class="yes" aria-label="yes">✓</td><td class="no" aria-label="no">✗</td></tr>
<tr><th scope="row">Unrestricted relation fields</th><td class="no" aria-label="no">✗</td><td class="yes" aria-label="yes">✓</td><td class="yes" aria-label="yes">✓</td><td class="yes" aria-label="yes">✓</td></tr>
<tr><th scope="row">Unrestricted relational operators</th><td class="no" aria-label="no">✗</td><td class="yes" aria-label="yes">✓</td><td class="yes" aria-label="yes">✓</td><td class="yes" aria-label="yes">✓</td></tr>
<tr><th scope="row"><code>one</code>, <code>lone</code>, <code>no</code> quantifiers</th><td class="no" aria-label="no">✗</td><td class="yes" aria-label="yes">✓</td><td class="yes" aria-label="yes">✓</td><td class="yes" aria-label="yes">✓</td></tr>
<tr><th scope="row">Scriptability (<a href="#sec6">section 6</a>)</th><td class="no" aria-label="no">✗</td><td class="yes" aria-label="yes">✓</td><td class="yes" aria-label="yes">✓</td><td class="no" aria-label="no">✗</td></tr>
<tr><th scope="row">LTL operators, infinite-trace semantics</th><td class="no" aria-label="no">✗</td><td class="no" aria-label="no">✗</td><td class="yes" aria-label="yes">✓</td><td class="yes" aria-label="yes">✓</td></tr>
<tr><th scope="row">Non-compositional shorthand</th><td class="no" aria-label="no">✗</td><td class="no" aria-label="no">✗</td><td class="no" aria-label="no">✗</td><td class="yes" aria-label="yes">✓</td></tr>
<tr><th scope="row">Global constraints, <code>sig</code>-specific constraints</th><td class="no" aria-label="no">✗</td><td class="no" aria-label="no">✗</td><td class="no" aria-label="no">✗</td><td class="yes" aria-label="yes">✓</td></tr>
</tbody>
</table>
  <figcaption><b>Table 1.</b> Language-level comparison. The three language levels form a gradual progression toward the expressive power of Alloy 6, while adding teaching-focused features such as explicit testing constructs (section <a href="#sec5">5</a>).</figcaption>
</figure>
<figure id="fig1">
  <pre><code><b>abstract sig</b> Player {}
<b>one sig</b> X, O <b>extends</b> Player {}
<b>sig</b> Board { board: <b>pfunc</b> (<b>Int</b> -&gt; <b>Int</b>) -&gt; Player }
<b>pred</b> wellformed {
  <b>all</b> b: Board | <b>all</b> row, col: <b>Int</b> | {
    (row &lt; 0 <b>or</b> row &gt; 2 <b>or</b> col &lt; 0 <b>or</b> col &gt; 2) <b>implies</b>
      <b>no</b> b.board[row][col] } }</code></pre>
  <figcaption><b>Figure 1.</b> Froglet example: boards in tic-tac-toe. There are exactly two players: <code>X</code> and <code>O</code>. Each board contains a partial function (<code>pfunc</code>) that maps row-column pairs to player names. The <code>wellformed</code> predicate constrains play to valid row and column indices.</figcaption>
</figure>
<figure id="fig2">
  <pre><code><b>sig</b> Node { edges: <b>set</b> Node -&gt; <b>Int</b> }
<b>pred</b> wellformed { <b>all disj</b> n1, n2: Node | <b>lone</b> n1.edges[n2] }
<b>pred</b> connected { <b>all disj</b> n1, n2: Node | n2 <b>in</b> n1.^(edges.<b>Int</b>) }</code></pre>
  <figcaption><b>Figure 2.</b> Relational Forge example: weighted directed graphs. Use of the join operator in the <code>connected</code> predicate allows easy removal of weights from the edge relation for use with transitive closure.</figcaption>
</figure>
<figure id="fig3">
  <pre><code><b>sig</b> Counter {var value: <b>one Int</b>}
<b>pred</b> someTrace { Counter.value = 0 <b>and</b>
  always { Counter.value' = add[Counter.value, 1] } }</code></pre>
  <figcaption><b>Figure 3.</b> Temporal Forge example: an increasing counter. The syntax is quite similar to Alloy 6; following linear temporal logic (LTL), expressions are evaluated with respect to an implicit time index; priming (<code>'</code>) references the next state. Thus, <code>someTrace</code> says that the counter initially holds <span class="sc">0</span> and advances by <span class="sc">1</span> in every step.</figcaption>
</figure>
<p>counterexamples can be a powerful teaching tool in security or networking classes. Industrial modeling, where instances may be huge and tied to specific domains, can also benefit from carefully-chosen visualizations. Indeed, one of the examples below (section <a href="#sec4.3">4.3</a>) is derived from a challenge posed by an expert Alloy user [<a href="#ref68" id="cite52" role="doc-biblioref">Zave 2020</a>], who said of the default Alloy visualization: “I never use it, believing (rightly or wrongly) from past experience that my models are too complex.” She</p>
<figure id="fig4">
  <div class="figbody figrow">
    <button type="button" class="zoom" data-full="images/img-008-002.png" aria-label="Enlarge Figure 4, image 1 of 2"><img src="images/img-008-002.png" alt="Figure 4, image 1 of 2" loading="lazy"></button>
    <button type="button" class="zoom" data-full="images/img-008-004.png" aria-label="Enlarge Figure 4, image 2 of 2"><img src="images/img-008-004.png" alt="Figure 4, image 2 of 2" loading="lazy"></button>
  </div>
  <figcaption><b>Figure 4.</b> Visualizing the example protocol. Left: Alloy with projection. Right: custom visualization via a sequence diagram. The middle agent in the diagram represents the medium of communication which, following <a href="#ref22" id="cite53" role="doc-biblioref">Dolev and Yao</a> [<a href="#ref22" id="cite55" role="doc-biblioref">1983</a>], is synonymous with the attacker.</figcaption>
</figure>
<p>further related [personal communication, used with permission] that she draws pictures by hand to debug models. Custom visualization can automate such drawings and make them interactive.</p>
<p>To motivate custom visualizations in a pedagogic setting, we use three examples: cryptographic protocol executions (section <a href="#sec4.1">4.1</a>), river-crossing puzzles (section <a href="#sec4.2">4.2</a>), and network reachability (section <a href="#sec4.3">4.3</a>). Each highlights issues with Alloy’s default visualization and shows how our custom version mitigates the problems. Crucially, none of the issues are solved by Alloy’s (useful and flexible) theming feature, which allows users to adjust presentation settings and project out some detail (e.g., showing only one system state at a time). We present results on student use in section 7.2.</p>
<h3 id="sec4.1"><span class="num">4.1</span> Example: Crypto Protocols</h3>
<p>Figure <a href="#fig4">4</a> visualizes a protocol execution instance between an initiator and a responder, with an attacker in between. The protocol has two steps: first, the initiator sends the responder’s name, encrypted with the responder’s public key; second, the responder replies with the initiator’s name, encrypted with the initiator’s public key.</p>
<p>The left subfigure shows Alloy’s default visualization with the “magic layout” feature applied and projected to one state. Even though projection allows a viewer to step through the protocol, it is unclear what, if anything, a viewer can learn from this without much tedious study. (The default table-based output is no better; there are 19 rows in one <code>learned_times</code> relation alone.) One might imagine filtering this flood of information via theming, e.g., by hiding encrypted terms that aren’t used in a given state. Unfortunately, because a term might be “used” in subtle ways (generated, used to decrypt, used to encrypt, learned from encryption, etc.) this is not currently possible to do consistently in Alloy’s visualizer.</p>
<p>In contrast, the right half of fig. <a href="#fig4">4</a> shows a custom visualization of the same instance in Forge, expanding on prior work with protocols in Sterling [<a href="#ref57" id="cite56" role="doc-biblioref">Siegel et al. 2021</a>]. It captures the standard imagery of protocol message-passing in the “Alice and Bob” style [<a href="#ref14" id="cite57" role="doc-biblioref">Caleiro et al. 2006</a>; <a href="#ref47" id="cite58" role="doc-biblioref">McCarthy and Krishnamurthi 2008</a>], with each of the four transitions represented as horizontal arrows. This <em>domain-specific format</em> allows a user to see the full execution of the protocol at once, while simultaneously eliding low-level detail that is at best unnecessary for the user to see.</p>
<h3 id="sec4.2"><span class="num">4.2</span> Example: River Crossing</h3>
<p>Figure <a href="#fig5">5</a> shows the default and a custom visualization for pairs of states in a river-crossing problem. Observe how easy it is to see the difference between the two states in the custom visualization, and how hard it is in the default; a reader can very easily miss all the differences—or even that there <em>are</em> any differences. Furthermore, the layout of atoms in the default visualization is based</p>
<figure id="fig5">
  <div class="figbody figrow">
    <button type="button" class="zoom" data-full="images/img-009-006.png" aria-label="Enlarge Figure 5, image 1 of 4"><img src="images/img-009-006.png" alt="Figure 5, image 1 of 4" loading="lazy"></button>
    <button type="button" class="zoom" data-full="images/img-009-010.png" aria-label="Enlarge Figure 5, image 2 of 4"><img src="images/img-009-010.png" alt="Figure 5, image 2 of 4" loading="lazy"></button>
    <button type="button" class="zoom" data-full="images/img-009-008.png" aria-label="Enlarge Figure 5, image 3 of 4"><img src="images/img-009-008.png" alt="Figure 5, image 3 of 4" loading="lazy"></button>
    <button type="button" class="zoom" data-full="images/img-009-012.png" aria-label="Enlarge Figure 5, image 4 of 4"><img src="images/img-009-012.png" alt="Figure 5, image 4 of 4" loading="lazy"></button>
  </div>
  <figcaption><b>Figure 5.</b> River crossing states. Left: default. Right: custom.</figcaption>
</figure>
<figure id="fig6">
  <div class="figbody figrow">
    <button type="button" class="zoom" data-full="images/img-009-014.png" aria-label="Enlarge Figure 6, image 1 of 3"><img src="images/img-009-014.png" alt="Figure 6, image 1 of 3" loading="lazy"></button>
    <button type="button" class="zoom" data-full="images/img-009-016.png" aria-label="Enlarge Figure 6, image 2 of 3"><img src="images/img-009-016.png" alt="Figure 6, image 2 of 3" loading="lazy"></button>
    <button type="button" class="zoom" data-full="images/img-009-018.png" aria-label="Enlarge Figure 6, image 3 of 3"><img src="images/img-009-018.png" alt="Figure 6, image 3 of 3" loading="lazy"></button>
  </div>
  <figcaption><b>Figure 6.</b> Different definitions of reachability in a single instance. Left: default visualization (showing all definitions). Right: custom visualization for two different definitions; a clickable menu allows the viewer to adjust which definition should be shown. Line colors vary to show different packet headers being processed differently (not currently possible via Alloy’s theming options).</figcaption>
</figure>
<p>on a generic graph layout and therefore does not reflect the actual location of objects. In the first state, the farmer is separated from the fox although they are on the near side of the river, and the chicken and fox are together despite being on opposite sides. The custom display shows the actual <em>river</em>, which is implicit in the model, and puts atoms on the correct sides of it.</p>
<h3 id="sec4.3"><span class="num">4.3</span> Example: Network Reachability</h3>
<p>Figure <a href="#fig6">6</a> visualizes a single instance for a model that contrasts four different definitions of network reachability. Because Alloy’s default visualizer produces directed graphs, one might think that it should do well; however, it does not.<a class="fnref" id="fnref2" href="#fn2" role="doc-noteref"><sup>2</sup></a><span class="sidenote" id="fn2" role="note"><span class="fnnum">2</span> During a live lab session at a <em>formal-methods</em> summer school where this exact instance appeared, one of the students was heard to say, “Oh, no, I don’t like this. Kill it with fire.” of the generic visualization (which appeared before the custom visualization loaded). We believe this illustrates well the emotional experience of even a formal-methods-interested student when first faced with such visual output.</span> This example highlights two issues:</p>
<ul>
  <li>The reachability relations contain tuples of the form (<em>hdr, src, dst</em>): a header that determines how the packet is forwarded, a source, and a destination. Alloy assigns the first element <em>hdr</em> to be the edge’s source, the third element <em>dst</em> to be the edge’s sink, and the middle element <em>src</em> (the actual source node) to be the edge label.</li>
  <li>Since the model represents physical links as discrete atoms, they are objects in the default visualization. Each link has a sender and receiver field, which are displayed as edges. But we would do much better to collapse each link object into a single direct edge.</li>
</ul>
<p>These issues could perhaps be fixed by expanding Alloy’s theming feature to let the user control edge-label assignment and collapse nodes into edges (rather than breaking the connection when links are hidden). However, when a student discovers a lack of theming power in their visualization, they are unlikely to spend the effort of researching and modifying Alloy’s code to support their vision. Instead, our experience shows that they will struggle to debug their model with the default visualizer. Another fix might be to change the basic structure of the model, perhaps by reordering packet tuples. Indeed, we ourselves do this sometimes, but the refactoring effort is significant. More importantly, elements of a model are usually there for a reason and sweeping changes often have unforeseen consequences (especially when the modeler is not yet experienced with debugging). Custom visualizations enable modifications while avoiding the need to refactor the model.</p>
<h2 id="sec5"><span class="num">5</span> Testing: From Rough Ideas to Reliable Models</h2>
<p>For students without experience in formal modeling, unit testing may be the only experience they have approaching <span class="sc">fm</span>; after all, a unit test is a point-wise specification. Thus, rather than disparaging unit tests for their incompleteness, we would do well to see them for what they are: a first step on the road to <span class="sc">fm</span>. Explicit support for different kinds of testing in a student’s model can help anchor their progression from expected input-output pairs to properties to pre- and post-conditions and beyond. We begin with some critique of testing in Alloy (section <a href="#sec5.1">5.1</a>) and then describe the design of testing in Forge (section <a href="#sec5.2">5.2</a>). Section <a href="#sec7.3">7.3</a> reports preliminary evaluation.</p>
<h3 id="sec5.1"><span class="num">5.1</span> Alloy Critique: Testing</h3>
<p>Testing in Alloy uses annotations on <code>run</code> and <code>check</code> commands. For example, a command telling Alloy to produce instances in which someone is married can be converted into a test by adding <code>expect 1</code> for “should be satisfiable” or <code>expect 0</code> for “should be unsatisfiable”:</p>
<pre><code><b>run</b> {<b>some</b> p: Person | <b>some</b> p.spouse} expect 1</code></pre>
<p>This lightweight idiom is useful, but has some notable flaws:</p>
<ul>
  <li><code>expect</code> serves two different purposes in Alloy. Not only does it label satisfiability expectations, it also doubles (as of version 6.1.0) as a way to configure symmetry breaking per <code>run</code>: <code>expect 1</code> disables it and <code>expect 0</code> enables it. Converting a <code>run</code> into a test can therefore alter its output, since symmetry breaking often eliminates many isomorphic instances.</li>
  <li>Alloy lacks a way to separate test cases into suites within a single file. Alloy can execute a single run or <em>all</em> runs, but often students are working on a specific area of their model and want to run some tests without waiting for all tests to finish (which may take minutes).</li>
  <li>Writing unit tests with concrete instances can help students understand assignments and reinforce the semantics of satisfiability. Unfortunately, Alloy lacks explicit syntax and optimizations for this. The main challenge is that, to define a non-trivial instance in Alloy, one usually needs to name individual atoms. This means either adding global constants via <code>one sig</code> declarations, or naming the atoms locally with disjoint quantification (<code>some disj x1, x2</code> . . .). E.g., to define an instance of a family-tree model, we could write:</li>
</ul>
<pre><code>  <b>one sig</b> Ani, Barbara, Cedric <b>extends</b> Person {}
Ani.mother = Barbara <b>and</b> Ani.father = Cedric <b>and</b> . . .</code></pre>
<p>or, alternatively:</p>
<pre><code><b>some disj</b> a, b, c: Person | a.mother = b <b>and</b> a.father = c <b>and</b> . . .</code></pre>
<p>Since <em>all</em> tests in a module must instantiate <em>all</em> <code>one sig</code> definitions, the global approach can result in confusing overlap between tests in the same file. If every test is in its own file, the global approach can work well, but at the added organizational cost of multiple files. The quantification method is more compact, but can suffer from poor performance. There has been work on adding better unit-test support to Alloy, such as AUnit [<a href="#ref59" id="cite60" role="doc-biblioref">Sullivan et al. 2018</a>], but these are not currently merged into the official tool.</p>
<figure id="fig7">
  <pre><code> 1  <b>pred</b> fullFirstRow {(Board.board[0]).X = (0+1+2)}
 2  <b>pred</b> someMoveTaken {<b>some</b> Board.board}
 3  ----- New Constructs: -----
 4  <b>inst</b> wellformed_instance {
 5      Board = `Board0
 6      Player = `X + `O
 7      X = `X   O = `O
 8      `Board0.board = (1, 1) -&gt; `X + (1, 2) -&gt; `O
 9  }
10  <b>example</b> moveMiddleFirst <b>is</b> {wellformed} <b>for</b> wellformed_instance
11  <b>test expect</b> { {someMoveTaken} <b>for</b> wellformed_instance <b>is</b> sat }
12  <b>test suite for</b> winning {
13      <b>assert</b> fullFirstRow <b>is sufficient for</b> winning <b>for</b> 1 Board
14      <b>assert</b> someMoveTaken <b>is necessary for</b> winning <b>for</b> 1 Board}</code></pre>
  <figcaption><b>Figure 7.</b> Testing constructs in Forge based on the tic-tac-toe model in fig. 1. The <code>example</code> checks that a specific board is considered wellformed. The <code>test</code> confirms that moves can be taken on this board. The assertions check that a specific pattern of moves implies a winner exists, and that no player can win until some moves are taken. The <code>winning</code> predicate, not shown due to space, encodes the 3-in-a-row criteria.</figcaption>
</figure>
<p>Finally, testing can be good for more than just validating an existing model. In the programming domain, tools like CodeWrite [<a href="#ref20" id="cite61" role="doc-biblioref">Denny et al. 2019</a>] and Examplar [<a href="#ref67" id="cite62" role="doc-biblioref">Wrenn 2022</a>] have shown that <em>executable examples</em> are a useful way to detect early misconceptions and provide students with immediate feedback—before they have written any code. They do this by running student tests against a hidden, known-correct (<em>wheat</em><a class="fnref" id="fnref3" href="#fn3" role="doc-noteref"><sup>3</sup></a><span class="sidenote" id="fn3" role="note"><span class="fnnum">3</span> As opposed to incorrect (<em>chaff</em> ) implementations. We adopt this terminology, although we use only wheats.</span>) implementation. Ideally, we would be able to borrow this idea from programming education to help students in a formal modeling context, but Alloy is not built to run tests against a hidden model.</p>
<h3 id="sec5.2"><span class="num">5.2</span> Design of Testing in Forge</h3>
<p>Forge languages support a number of testing constructs (fig. <a href="#fig7">7</a>):</p>
<figure id="fig8">
  <div class="figbody figrow">
    <figure class="subfig">
      <button type="button" class="zoom" data-full="images/fig8a.png" aria-label="Enlarge the Forge architecture diagram"><img src="images/fig8a.png" alt="Forge architecture: a visualizer over a surface language over a core language over the Pardinus solver, with custom visualization and navigation feeding the visualizer, and a domain model compiling through helper predicates and #lang to the solver." loading="lazy"></button>
      <figcaption>(a) Forge architecture</figcaption>
    </figure>
    <figure class="subfig">
      <pre><code>#lang forge/core
(set-option! 'problem_type 'temporal)
(sig Counter)
(relation value (Counter Int) #:is-var "var")
(pred someTrace (and
  (= (join Counter value) (int 0)))
  (always (= (join Counter (prime value))
             (add (join Counter value) (int 1)))))
(run someTrace_run #:preds [someTrace])
(display someTrace_run)</code></pre>
      <figcaption>(b) Core Forge version of a temporal program (<a href="#fig3">fig. 3</a>)</figcaption>
    </figure>
  </div>
  <figcaption><b>Figure 8.</b> Forge consists of several layers. Its languages compile to a common core.</figcaption>
</figure>
<dl>
  <dt>Examples</dt>
  <dd>(line 4) are concrete instances that should satisfy a given formula. Educationally, these correspond to unit tests and tend to be used early on in the modeling process (“Here is what I think should happen. Does it look right?”). For reasons related to how examples are implemented (section <a href="#sec6">6</a>), the example construct is currently only available in Froglet and Relational Forge, not in Temporal Forge.</dd>
  <dt>Assertions</dt>
  <dd>(lines 11–12) are normative statements about implication between predicates. They are extremely constrained by design, and can only express whether one predicate is <em>necessary</em> or <em>sufficient</em> for another. Educationally, these (roughly) correspond to property-based tests. (“Is an undirected tree always a directed tree?”)</dd>
  <dt>Test Blocks</dt>
  <dd>(line 9) are a less limited form of assertions that state a given run will be either satisfiable or not. They are useful in cases where assertions do not suffice, such as when a student wants to check that a property is non-vacuous. (“Can my transition system even run?”) <em>Test blocks most closely resemble the style of testing in Alloy.</em></dd>
  <dt>Suites</dt>
  <dd>(line 10) group tests within the same file. Each suite comes with a label (typically the name of a predicate); Forge warns the user if this label does not appear in the enclosed tests.</dd>
</dl>
<p><em>Testing early.</em> Forge provides the ability to run all of these testing constructs against hidden known-correct models that course staff can distribute with assignment handouts. If a student’s test flags the known-correct solution as erroneous, it is likely that their understanding of the problem is invalid. In either case, students receive an instance illustrating the mismatch.</p>
<h2 id="sec6"><span class="num">6</span> Architecture and Implementation</h2>
<p>Forge is built atop Racket [<a href="#ref30" id="cite63" role="doc-biblioref">Felleisen et al. 2015</a>], with a slightly-modified Pardinus backend [<a href="#ref44" id="cite64" role="doc-biblioref">Macedo et al. 2022</a>] and modified Sterling for visualizing instances [<a href="#ref25" id="cite66" role="doc-biblioref">Dyer and Baugh 2021</a>]. Racket provides a toolkit for building languages. Forge takes particular advantage of its tools for <span class="sc">ide</span> support and custom error messages. Pardinus is a cutting-edge solver. Forge was an early adopter, and Alloy later integrated Pardinus in Alloy 6. Sterling displays instances found by Pardinus in an interactive Web page. Forge adds helpers to ease the creation of custom visualizations.</p>
<p>Figure 8a shows the architecture in more detail. Each language level contains its own surface syntax, error messages, and expander that maps its syntax to a <em>core Forge</em> language. For instance, fig. 8b shows the core-language version of the Temporal Forge program from fig. 3. The core language is implemented as a Racket library; students do not need to engage with this core syntax unless they wish to.</p>
<p>Semantically, the core and surface versions are identical. However, the core language provides a convenient target for Racket macros and other Forge sub-languages. Because of this, Forge is <em>scriptable</em>: students can write Racket programs to do anything from counting instances to performing counterexample guided synthesis. We have also used this facility to create <em>domain-specific</em> modeling languages (section <a href="#sec9">9</a>). However, we have not yet built and deployed enough of these languages to fully understand their pedagogic implications.</p>
<p><em>Performance.</em> Because Forge is built on the same solver engine as Alloy 6, its performance is comparable to Alloy’s in most respects. However, there are differences:</p>
<ul>
  <li>When run, Forge models execute as Racket programs—meaning that there is a 1–2 second delay while the Racket process loads. We plan to fix this issue for 2024 by changing the architecture to use a persistent worker process, much like Alloy does with Java.</li>
  <li>Forge provides support for explicit partial instances (similar to <a href="#ref48" id="cite67" role="doc-biblioref">Montaghami and Rayside</a> [<a href="#ref48" id="cite68" role="doc-biblioref">2012</a>]), which can greatly improve the solving speed on some problems. However, partial instances cannot yet be specified at the per-state granularity in Temporal Forge (hence why <code>example</code> is unavailable there, since <code>example</code> is implemented via partial instances). This limitation is because partial instances are embodied in the upper and lower bounds passed to the solver, which apply to <em>all</em> states in a solution trace. Thus, while partial instances can still be used for optimization in Temporal Forge, fine-grained control is not yet possible.</li>
</ul>
<h2 id="sec7"><span class="num">7</span> Evaluation</h2>
<p>We evaluate Forge along the three core dimensions presented in this paper: language levels (section <a href="#sec7.1">7.1</a>), custom visualization (section <a href="#sec7.2">7.2</a>), and testing (section <a href="#sec7.3">7.3</a>). The formal evaluation is based on two semesters—Spring 2022 (92 students) and Spring 2023 (64 students)—of teaching with Forge in <span class="sc">l4s</span>. We remark that we have deployed versions of Forge in <em>five</em> semesters—which have enabled us to refine the above ideas—and several smaller events (e.g., summer schools), but do not have rigorous data from those experiences. The remarks in section <a href="#sec2">2</a> about our students’ backgrounds apply to our survey participants.</p>
<p>Since our survey instruments collected a variety of data, we used several methods to conduct the analysis. For quantitative data, we built tables and graphs like those shown below. For qualitative data, three authors worked together to categorize responses using standard practices. One author proposed initial labels for the data, the others reviewed the codes, and the team revised the labels if needed to reach agreement. Our artifact contains all the survey instruments used in the evaluation.</p>
<h3 id="sec7.1"><span class="num">7.1</span> Evaluation: Language Levels</h3>
<p>Having created language levels and deployed them in the classroom, the obvious question is: are they effective? Just in terms of course structure, splitting the language was beneficial. In particular, Froglet let the <span class="sc">l4s</span> course (which has no discrete math prerequisite) replace a first assignment that simply drilled relational operators with a realistic modeling exercise. But here we look deeper.</p>
<p>To determine the concrete impacts on students, we investigate the following research questions: RQ1. To what extent are students able to model topics of interest in the early, less expressive language levels? RQ2. What preconceptions do students have <em>before</em> moving to a new language level? RQ3. What difficulties do students face <em>after</em> transitioning from one language level to another?</p>
<h4 id="sec7.1.1"><span class="num">7.1.1</span> RQ1: Expressive Power.</h4>
<p>There are three types of modeling assignment in l4s: homeworks, labs, and projects. While homeworks and labs are tailor-made to fit the current language level, projects are free-form. Students form groups of two or three and model any domain of their choosing. They receive guidance and feedback on proposed topics, but the specifics are entirely their own. Naturally, their choices may conflict with the design for the current language levels.</p>
<p>There are two projects, a midterm and a final. The midterm takes place a few days after the switch from Froglet to Relational Forge; Temporal Forge is not yet available. The final takes place after the switch to Temporal Forge. Students were encouraged to use Froglet on the midterm, but could switch to Relational Forge after meeting with a staff member. Students could use any language on the final. During the weeks-long final project, students met twice with course staff to report their progress and possibly receive suggestions; at these meetings, course staff may have recommended a certain language.</p>
<p>Chosen topics are naturally colored by the modeling experience students have had so far, but we believe that the breadth of topics and students’ ability to execute their vision in a given language still gives us a valuable perspective on the expressive power of the early language levels.</p>
<p><em>Results.</em> Table <a href="#tab2">2</a> details the languages students used on their projects. Midterm projects were mostly done in Froglet (59 of 77 across both years) and included diverse topics such as: board games, fast-food orders, chemical reactions, sports, algorithms, and data structures. For groups who chose Relational Forge, the sticking point with Froglet was the lack of support for sets. For example, a</p>
<figure id="tab2">
  <div class="table-pair">
<table>
<caption>2022</caption>
<thead><tr><th scope="col">Language level</th><th scope="col">Midterm</th><th scope="col">Final</th></tr></thead>
<tbody>
<tr><th scope="row">total</th><td>45</td><td>33</td></tr>
<tr><th scope="row">Froglet</th><td>36</td><td>0</td></tr>
<tr><th scope="row">Relational</th><td>8</td><td>18</td></tr>
<tr><th scope="row">Temporal</th><td>N/A</td><td>13</td></tr>
<tr><th scope="row">SMT</th><td>1</td><td>2</td></tr>
</tbody>
</table>
<table>
<caption>2023</caption>
<thead><tr><th scope="col">Language level</th><th scope="col">Midterm</th><th scope="col">Final</th></tr></thead>
<tbody>
<tr><th scope="row">total</th><td>32</td><td>26</td></tr>
<tr><th scope="row">Froglet</th><td>23</td><td>2</td></tr>
<tr><th scope="row">Relational</th><td>9</td><td>8</td></tr>
<tr><th scope="row">Temporal</th><td>N/A</td><td>13</td></tr>
<tr><th scope="row">SMT</th><td>0</td><td>3</td></tr>
</tbody>
</table>
</div>
  <figcaption><b>Table 2.</b> Language levels that students chose for their projects. SMT projects used an SMT solver such as Z3 [<a href="#ref18" id="cite69" role="doc-biblioref">de Moura and Bjørner 2008</a>] instead of Forge.</figcaption>
</figure>
<p>group modeling Dijkstra’s shortest-path algorithm found it convenient to store the (weighted) edge relation as a field of type <code>set Node -&gt; Node -&gt; Int</code> rather than emulating the relation as a partial boolean-valued function.</p>
<p>Most final projects used either Relational Forge (26 of 59 across both years) or Temporal Forge (also 26 of 59 across both years). Final project submissions were always more technically demanding than the midterms. Projects included OS memory management, grammar trees, and air traffic control; fig. <a href="#fig11">11</a>, which appears in section <a href="#sec7.2">7.2</a>, gives a longer list of final project topics.</p>
<p>A handful of groups (1 midterm and 5 finals across both years) used an SMT solver for their projects. Usually these projects needed features that neither Forge nor Alloy provide (e.g., soft constraints). In one case (Minesweeper in 2023), the group switched for performance reasons caused by the fact that Forge (like Alloy) uses only bit-vector arithmetic, which can be slower than what SMT provides via theory solvers.</p>
<p><em>Interpretation.</em> Froglet seems to suffice for most students’ first self-directed foray into modeling. Most midterm projects did not need relations, and all but 17 (<span class="sc">22 %</span>) of the others could encode relations as boolean-valued functions in Froglet. Froglet did not suffice for weighted graph algorithms. We believe this is an acceptable limitation because students had experience with Relational Forge at this point in the semester and could switch to it; still, it may be worthwhile to consider adding library functions for weighted graphs (analogous to the Froglet <code>reachable</code> helper). Anecdotally, the variety and scope of midterm projects compare favorably to the years before Forge was in use. Froglet may have enabled more-ambitious projects earlier by simplifying the language.</p>
<p>The final projects used a combination of Relational Forge (<span class="sc">44 %</span> overall) and Temporal Forge (also <span class="sc">44 %</span> overall), with the few remaining using Froglet or SMT. We attribute the even split to two competing factors: the familiarity of Relational Forge and the expressiveness of Temporal Forge. Students were inclined toward Relational Forge because they had more experience with it at the time when project proposals were due. Temporal Forge was a compelling option because of its convenience for modeling systems that change over time—a common theme of the course.</p>
<h4 id="sec7.1.2"><span class="num">7.1.2</span> RQ2: Preconceptions.</h4>
<p>Moving from one language level to the next requires students to adapt to major semantic changes. With Relational Forge, sets become the sole datatype in the language. With Temporal Forge, instances become infinite-trace lassos. These shifts can present a roadblock to learners if done poorly.</p>
<p>To ease the transitions between language levels, we used surveys and in-class discussions to identify preconceptions and address them <em>before</em> the class changed languages. For the surveys, students worked in pairs to assess possible behaviors for a semantic construct. E.g., the question in fig. <a href="#fig9">9</a> asks students currently using Froglet to rate possible outcomes for a join (<code>.</code>) in Relational Forge. Ratings used two dimensions (adapted from <a href="#ref61" id="cite70" role="doc-biblioref">Tunnell Wilson et al.</a> [<a href="#ref61" id="cite71" role="doc-biblioref">2018</a>]): is the outcome something you <em>expect</em> or not (e.g., an error might be surprising), and is the outcome something</p>
<figure id="fig9">
  <div class="figbody">
    <button type="button" class="zoom" data-full="images/fig9matrix.png" aria-label="Enlarge the survey question"><img src="images/fig9matrix.png" alt="Survey question. Prompt: run { some c: Course | c in c.prereqs }. Respondents rate four outcomes (SAT, UNSAT, an unknown-field error, and a course-cannot-be-its-own-prereq error) on a four-point scale from expected and liked to unexpected and disliked." loading="lazy"></button>
    <button type="button" class="zoom" data-full="images/img-015-021.png" aria-label="Enlarge the response chart"><img src="images/img-015-021.png" alt="Bar chart of the 2023 responses to the question above, grouped by outcome and coloured by the four expected/liked combinations." loading="lazy"></button>
  </div>
  <figcaption><b>Figure 9.</b> Example pre-Relational-Forge survey question and responses from 2023.</figcaption>
</figure>
<p>you <em>like</em> or not (e.g., an error might be helpful despite at first being surprising). The advantage of separating these dimensions is in forcing respondents to separate their knowledge of the language (<em>expected</em>) from their opinions about it (<em>liked</em>). We also asked students to write in an outcome if they preferred one that was not listed.</p>
<p>Figure <a href="#fig9">9</a> presents one question from the Relational Forge survey and the responses from 2023. Forge returns <code>satisfiable</code> (<code>SAT</code>) for this prompt. The responses show that most students <em>expect</em> this outcome, but roughly a third of them <em>dislike</em> it and instead prefer an error. Students who do not expect a <code>SAT</code> outcome can use this example to learn why Relational Forge behaves the way it does.</p>
<p><em>Results: Froglet to Relational Forge.</em> For the Froglet-to-Relational-Forge transition, we obtained 77 responses from 2022 and 61 from 2023. The questions focused on three features that are present in Relational Forge but inexpressible in Froglet: can a singleton be contained in another singleton (e.g., <code>person in c.instructor</code>); can a singleton be equal to a set (e.g., <code>person = c.TAs</code>); and what behavior should reversing the dot operator produce (e.g., <code>CS2 in prereqs.CS1</code>)? Across both years, for each of the above questions, students preferred some error behavior the most (e.g., expected and liked “Error: Cannot compare a person and a set.”). Free-form comments indicated a strong call for type errors (“set[X] is a different type than X itself.”) from 43 (<span class="sc">56 %</span>) in 2022 and 20 (<span class="sc">33 %</span>) in 2023. Flipped join attracted many negative comments, from 21 (<span class="sc">27 %</span>) in 2022 and 6 (<span class="sc">10 %</span>) in 2023, some of which were quite strong (“What a travesty that would be.”) and led to lively and productive discussions about why the relational semantics is useful for lightweight <span class="sc">fm</span>.</p>
<p><em>Interpretation.</em> The survey responses highlight ways that modeling with relations is more of a leap than modeling with functions for students used to programming with objects, with many <em>unexpected</em> and <em>disliked</em> behaviors relative to that prior experience. Survey comments informed followup lecture content to clarify points of confusion. More generally, the survey revealed a preference for noisy failures over silent ones (error rather than <code>unsat</code>), which motivates future work on all Forge languages (section <a href="#sec9">9</a>).</p>
<p><em>Results: Relational Forge to Temporal Forge.</em> For the Relational-to-Temporal transition, we obtained 71 responses from 2022 and 59 responses from 2023. The survey focused on the meaning of four temporal operators: <code>eventually</code>, <code>always</code>, <code>until</code>, and <code>next_state</code> (in LTL: F, G, U, X). Students had no prior exposure to these operators and the survey did not introduce them; its purpose was to identify potential upcoming misconceptions stemming from the English-language names for the operators. Each survey question presented a formula, a trace describing a system, and several possible outcomes of matching the trace against the formula. We adapted this format from <a href="#ref33" id="cite72" role="doc-biblioref">Greenman et al.</a> [<a href="#ref33" id="cite73" role="doc-biblioref">2023</a>]. Traces were given in graphical form, not via Forge syntax.</p>
<p>We found similar responses and misconceptions to what the prior authors uncovered; e.g., students can be confused about the meaning of a formula without a temporal operator attached, often prepending an implicit <code>always</code>. We also observed confusion about whether <code>next_state</code> applies to one state or to several. <a href="#ref56" id="cite74" role="doc-biblioref">Saarinen</a> [<a href="#ref56" id="cite75" role="doc-biblioref">2021</a>] observed this issue but <a href="#ref33" id="cite76" role="doc-biblioref">Greenman et al.</a> [<a href="#ref33" id="cite77" role="doc-biblioref">2023</a>] did not; perhaps the issue is common among beginners but easy to correct.</p>
<p>One surprising outcome is an apparent mixup about functions versus formulas. For example, on the formula <code>next_state{next_state{eventually{Red}}}</code>, a student commented: “I feel like it doesn’t really make sense to call <code>next_state</code> on <code>eventually</code> because <code>eventually</code> should <em>already evaluate to true or false</em>, and there is no actual formula for <code>next_state</code>.” (emphasis ours). In fact there is no “call”, and the <code>eventually</code> subformula does not evaluate to a boolean before the <code>next_state</code> operator is evaluated. This mixup is surprising because students had spent almost two months working in Froglet and Relational Forge, where quantifiers are evaluated similarly to temporal operators. It would therefore seem that claims of conceptual transfer from first-order quantification to <em>temporal</em> quantification are ill-founded in some cases; students may default to their programming intuitions even in a formal logic context.</p>
<h4 id="sec7.1.3"><span class="num">7.1.3</span> RQ3: Difficulties Using New Language Levels.</h4>
<p>After each language change, we asked students to complete in-class surveys about stumbling blocks they encountered with each new language compared to the previous language level. Our goal was to identify specific issues qualitatively.</p>
<p><em>Results: Relational Forge.</em> We obtained 54 Relational Forge responses. While a few students preferred working in Froglet (“The change to everything being treated as a set really threw me off.”), most were happy with Relational Forge. One student wrote that Relational Forge is “a lot more useful and intuitive”; a few others appreciated its set-based semantics (“the fact that the underlying machinery in Forge is sets makes it all the better since I come from a more mathematical background.”). Yet, there were also many reports of trouble with relational operators (“it took me a while to really understand some of the operators like the dot operator and transitive closure operator and that everything was a set”; “especially <code>-&gt;</code> and <code>^</code> were tough [...] getting problems with arity is hard to picture.”).</p>
<p>One survey question asked which language students would use now if they could redo their midterm project. Whereas only nine midterm groups used Relational Forge (table <a href="#tab2">2</a>), 29 respondents chose Relational Forge. These numbers suggest that students were very comfortable with Relational Forge after the transition. Another six chose a mix of languages and eight students did not have a strong opinion.</p>
<p><em>Results: Temporal Forge.</em> We received 32 Temporal Forge responses. Student opinions of Temporal Forge were strongly positive overall: 17 responses preferred working in the temporal language (“Writing transition statements in normal Forge was a confusing mess. On the other hand, these transitions were much easier to write (and then later read!) in Temporal Forge.”; “Having to specify a ‘State’ sig for (almost) every model was tedious, and I appreciate how Temporal Forge handles state for you.”). If they could revisit their midterm project, 13 responding students (nearly <span class="sc">41 %</span>) would have used Temporal Forge. This is encouraging with regard to the value of Temporal Forge, and the temporal fragment of Alloy 6, in teaching contexts.</p>
<p>Students did raise some concerns about the conceptual load of infinite traces (“I think understanding the counterexamples is harder, because it could involve infinite states and loops, and we’d need to go through all the states to find the actual contradicting state.”; “The most confusing concept for me in Temporal Forge was understanding lasso traces; I was particularly confused with how this prevented us from modeling deadlocks.”) and how the expression evaluator worked in the presence of implicit traces (“Harder to use the evaluator because you have to use next state.”). One student reported confusion with the priming operator, which delays the interpretation of a sub-expression until the next state: “It is counter intuitive to me that accessing a field of a Sig in the future does not actually return that Sig’s field. E.g. <code>Person '.Name</code> != <code>Person.Name '</code>”. This comment highlights a way that relations and temporal operators can combine awkwardly—especially when programming intuitions are applied.</p>
<p><em>Interpretation.</em> Concepts like transitive closure remain challenging even halfway through the semester, pointing to the potential value of built-in helpers like <code>reachable</code> even in less restricted languages. Responses did not give a clear answer to whether the <em>exact</em> restrictions of Froglet are ideal, but it seems clear that some restrictions on the language in the beginning are helpful. In terms of pedagogy, it could be worthwhile to reveal the set-based nature of Forge earlier, while the linguistic restrictions of Froglet are still in effect.</p>
<p>Students found Temporal Forge appealing, but unsurprisingly reported that transitioning to an infinite-trace semantics was difficult. The semantics of priming, especially, were reported as causing confusion. Syntactic checks to spot misuse of priming and other operators (similar to current checks for join) would be helpful in both Temporal Forge and Alloy.</p>
<h3 id="sec7.2"><span class="num">7.2</span> Evaluation: Custom Visualization</h3>
<p>We have three research questions about the impact of custom visualization on students: RQ1. What benefits and frustrations impact students as <em>consumers</em> of custom visualizations written by others? RQ2. What benefits and frustrations impact students as <em>producers</em> of their own visualizations? RQ3. What custom visualizations do students actually create, and what sorts of tools would ease their creation in the future? The first question gives us insight into the value of custom visualizations, separate from the overhead of creating one. This is vital for assignments and presentations in a formal-methods course, and enables the use of <span class="sc">fm</span> tools like Forge in other contexts such as security or distributed systems. The remaining two questions help us understand how the process of authoring custom visualizations could be improved.</p>
<h4 id="sec7.2.1"><span class="num">7.2.1</span> Experimental Setup.</h4>
<p>We had two experimental phases. In both 2022 and 2023, students received example visualizations for four modeling activities: the 𝑛-queens problem, a pair of river-crossing puzzles, the dining-philosophers problem, and tic-tac-toe games. The course staff provided instruction on building visualizations with demos in class, a tutorial document, and office hours.</p>
<p>In 2022, students were required to produce a custom visualization on their final project (or request an exemption; only 3 of the 27 groups did so). After the semester ended, we sent out a brief survey to collect feedback with which to improve the visualizer. In 2023, we added a library to Sterling called D3FX that helps with the visualization of tables and other common patterns. The final and midterm projects suggested—<em>but did not require</em>—that students make their own visualizations, which allowed us to evaluate patterns of use without coercion. Students completed a required reflection after finishing their work. They also completed surveys after using each of our four example visualizations.</p>
<h4 id="sec7.2.2"><span class="num">7.2.2</span> Formative Results.</h4>
<p>Students submitted 24 custom visualizations in 2022, covering a variety of domains including card games, group theory, graph algorithms, and election systems. We found several common elements among the visualizations:</p>
<ul>
  <li><strong>Domain-specific layouts</strong>, like the sequence diagrams in section <a href="#sec4.1">4.1</a>, were common. Binary trees, sports-field and board-game layouts, and even group theory have well-understood visual idioms that students tended to use (or were frustrated by difficulties creating).</li>
  <li><strong>Positional factors</strong>, like those in river-crossing puzzles (section <a href="#sec4.2">4.2</a>) were common. Students modeling binary trees needed the left and right children of a node to be positioned properly, those modeling sports fields had a layout in mind, and so on.</li>
  <li>Some students added <strong>interactive</strong> elements, such as custom buttons to explore a trace.</li>
  <li>Finally, <strong>tables</strong> appeared in a variety of contexts. Students made custom tables to see a game’s full progression over time, to organize a weekly schedule, or to arrange a panel of buttons.</li>
</ul>
<p>After the semester ended, we sent out an exit survey and received six responses. When asked for (non-exclusive) reasons for frustration or lack of success, students selected “limited time” (5 responses), “lack of JavaScript experience” (3 responses), and “issues with D3 or other data visualization framework” (1 response). We received three free-form responses, which asked for improved documentation and reported bugs in visualizations. Lack of JavaScript experience was also a major factor at office hours, pointing to the need to simplify the task of creating visualizations.</p>
<h4 id="sec7.2.3"><span class="num">7.2.3</span> RQ1: Benefits and Frustrations as a Consumer.</h4>
<p>For experiences with using the custom visualizations students were given, we conducted in-class surveys immediately after assignment deadlines. We present representative quotes and takeaways below.</p>
<p class="runin">Benefits:</p>
<ul>
  <li><strong>Untangling the default:</strong> Some students found the default visualization challenging and time-consuming to read (“The [default graph] was very messy and hard to read, so a custom one was pretty much required.”). It is worth noting that Sterling’s default is an improvement over Alloy’s (see <a href="#ref24" id="cite78" role="doc-biblioref">Dyer</a> [<a href="#ref24" id="cite79" role="doc-biblioref">2020</a>]). The custom visualizations were especially valuable on assignments (“This visualization made it much easier to actually understand the instance.”) even if the design was crude (“Although it was not very pretty to look at it did the job.”). <em>Takeaway: Students</em> <em>find custom visualizations to be helpful enough to merit their inclusion in assignments.</em></li>
  <li><strong>Domain-specific idioms:</strong> Many students appreciated domain-specific idioms. For example, being able to visualize an entire trace at once was useful (“The frame by frame linear visualization of different states was very helpful and something that is missing from Forge’s default visualizer.”). They reported that this helped to keep track of different objects (“easier to track movements of individual [goats and wolves].”), but wished for a clearer presentation of state-to-state changes (“I would appreciate arrows or some kind of emphasis on what changed in the transition between states.”). <em>Takeaway: Students find domain-specific display</em> <em>formats and other non-standard visual idioms useful, when they are appropriate. When</em> <em>presenting multiple states at once, it is useful to highlight changes between each.</em></li>
  <li><strong>Debugging or manual validation:</strong> Some students used the custom visualizer for debugging on homeworks ( “Our implementation initially failed, by observing the visualization we know it would get to a deadlock.”). Others reported that they were able to use the default table view to debug, only reaching for the custom visualizer at the end of the assignment (“I didn’t use it for debugging really but for verification of my results.”). <em>Takeaway: Custom</em> <em>visualizations are often (but not always) useful for debugging. Even when they are not, they</em> <em>can still aid manual validation.</em></li>
</ul>
<p class="runin">Frustrations:</p>
<ul>
  <li><strong>Unnecessary customization:</strong> Some students reported that they continued to use the default, especially on simple assignments (“I think with these [river-crossing] models the visualization isn’t completely necessary. I didn’t personally use it.”) <em>Takeaway: Not everyone</em> <em>will find custom visualizations useful.</em></li>
  <li><strong>Misleading names:</strong> Many of the frustrations students encountered were due to specific issues with the visualizers that we provided. Object labels were sometimes ambiguous (“hard to check if it was a certain animal’s crossing pattern that was causing the issue, or if we were magically making a new animal.”). This led to some students finding the river-crossing visualizer “basically useless.” Students were also confused when the same label (“R”) was used for two different things (“I was a bit confused with the use of R in the visualization. [...] it represented that they were holding their right chopstick, but for the chopstick sigs, it meant that a chopstick was requested.”). Finally, a lack of naming was sometimes also an issue (“it did not label WHICH goat/wolf was moving.”). <em>Takeaway: ensure</em> <em>consistent labeling of objects across state visualizations, and avoid ambiguity in labeling.</em></li>
  <li><strong>Implicit ordering:</strong> Implicit ordering in object names caused some students confusion (“I initially thought that the ordering of the smiths represented their order in the table, but it does not. I think putting the Smiths in order would make the visualization even more helpful.”). <em>Takeaway: ensure that any ordering on objects, including the ordering on names</em> <em>(e.g.,</em> <code>Person0</code><em>,</em> <code>Person1</code><em>), is clearly reflected in the visualization. Moreover, important spatial</em> <em>information, such as the circular ordering on seats at a round table, should be explicit.</em></li>
  <li><strong>Display bugs:</strong> Some students experienced issues with the visualization environment itself. Text was sometimes cut off or scrolling made difficult (“the time text display is cut off by default, leading me to think that something was broken with my time variable.”; “Sometimes the visualization will be too big to fit on the page.”). The visualization UI itself could also be frustrating (“I wasn’t aware that after we click next, we need to re-click <code>Run</code> every time to see the script applied.”) <em>Takeaway: while the UI was functional, further quality-of-life</em> <em>development is needed.</em></li>
  <li><strong>Lack of robustness to deviation:</strong> Finally, and most importantly, a visualization must be robust against buggy models. Course staff built visualizations with reference to a known-correct model, but students applied these visualizations to their own models. Naturally, students visualized imperfect models, revealing lack of robustness in our visualizer (“before my model was working, the arrows were pointing in the wrong direction.”; “I think it would be useful to omit the arrows until a model is correct.”; “I don’t trust it as a way to verify that my code is correct.”). E.g., our reference model disallowed a boat from crossing the river without any occupants, and so our visualizer produced confusing results if a student’s model did not do the same. <em>Takeaway: visualizations should be robust against incomplete</em> <em>models and other issues that may arise, and must not be misleading in such cases.</em></li>
</ul>
<h4 id="sec7.2.4"><span class="num">7.2.4</span> RQ2: Benefits and Frustrations as a Producer.</h4>
<p>The retrospective surveys also uncovered useful information about producing visualizations for the midterm and final projects.</p>
<p class="runin">Benefit:</p>
<ul>
  <li><strong>Building own visualizations:</strong> Students who built custom visualizations echoed the positive sentiments in section <a href="#sec7.2.3">7.2.3</a> (“It was just better for being able to picture how our model was doing. It was very difficult to tell if it was behaving properly in tabular form.”; “The visualization uses images of cards, which is so much more intuitive”; “I made the visualization mainly to help with debugging the Forge model and for my own personal purposes.”). The group who produced the ambitious Rust model in fig. <a href="#fig10">10</a> found visualization</li>
</ul>
<figure id="fig10">
  <div class="figbody figrow">
    <button type="button" class="zoom" data-full="images/img-020-023.png" aria-label="Enlarge Figure 10, image 1 of 2"><img src="images/img-020-023.png" alt="Figure 10, image 1 of 2" loading="lazy"></button>
    <button type="button" class="zoom" data-full="images/img-020-025.png" aria-label="Enlarge Figure 10, image 2 of 2"><img src="images/img-020-025.png" alt="Figure 10, image 2 of 2" loading="lazy"></button>
  </div>
  <figcaption><b>Figure 10.</b> Visualizing instances from student-authored final project on modeling ownership in Rust. Default (left) versus custom (right, Raw D3). Images used with permission from Thomas Castleman and Ria Rajesh.</figcaption>
</figure>
<p>instrumental to their success: “Without custom visualization, I don’t think we could have done this.” <em>Takeaway: Students found it worthwhile to produce their own visualizations.</em></p>
<p class="runin">Frustrations:</p>
<ul>
  <li><strong>Time investment:</strong> By far the most common issue reported (21 of 85 responses) was the time involved in making a custom visualization (“It seemed really complicated and we preferred to spend more time trying to understand our model better and making sure it worked through tests than just visuals.”; “ultimately we ran out of time/chose to spend it on other things like testing and debugging.”). One respondent who made a custom visualization said they would revert to the Forge default in the future. <em>Takeaway: Reduce the time needed</em> <em>to make a visualization.</em></li>
  <li><strong>JavaScript:</strong> Even with our 2023 improvements and D3FX helper library (section <a href="#sec7.2.1">7.2.1</a>), students had trouble programming their visualizers in JavaScript. Some had trouble uncovering the types of environment variables (“it made references to unbound variables that seemingly shouldn’t exist but were injected by Forge, and it was difficult to know what the types of these variables would be.”). Others asked for further documentation (“we ran out of time and thought there wasn’t enough resources for us to learn / figure out how to create one.”). One student reported that visualizers were “Impossible to debug.” At least one group started their visualizer using the helper library and then switched to other options later in the project (“when using D3FX, we ran into some issues with alignment [...]. Switching to plain D3 gave us control.”). <em>Takeaway: JavaScript (which students were</em> <em>not required to know) is a barrier for students and teaching it should not be a priority in a</em> <em>formal-methods course. Forge should adjust how simple visualizations are written so that even</em> <em>a helper library is unnecessary.</em></li>
</ul>
<h4 id="sec7.2.5"><span class="num">7.2.5</span> RQ3: Kinds of Visualizations.</h4>
<p>Figure <a href="#fig11">11</a> presents a showcase of 2023 final project topics and associated visualizations. There were 26 projects in total and 18 created some amount of custom visualization. Three groups used the Z3 [<a href="#ref18" id="cite80" role="doc-biblioref">de Moura and Bjørner 2008</a>] SMT solver, and so did not interact with Sterling; another 5 used the default table or graph view exclusively. Of the 18 groups that did create a custom visualization, 6 used the helper library (D3FX) we provided. Another 6 used D3 directly (Raw D3). On inspection, 5 of the Raw D3 visualizations were adapted from similar staff-provided examples that used D3. The other Raw D3 group created an ambitious visualization of</p>
<p class="caption">(a) Spikeball (D3FX) (b) Uno (D3FX) and Triple Triad (<code>div</code>-based) (c) Texas Hold’em (<code>div</code>-based)</p>
<figure id="fig11">
  <div class="figbody figsplit">
    <div class="figtable">
      <table>
<thead><tr><th scope="col">Title</th><th scope="col">Visualization</th></tr></thead>
<tbody>
<tr><th scope="row">2048</th><td>D3FX</td></tr>
<tr><th scope="row">Air Traffic Control</th><td>D3FX</td></tr>
<tr><th scope="row">Among Us</th><td><strong>Default</strong> Table</td></tr>
<tr><th scope="row">Chopsticks Game</th><td><strong>Default</strong> Table</td></tr>
<tr><th scope="row">Chopsticks Game (1)</th><td>D3FX</td></tr>
<tr><th scope="row">Chromatic Sudoku</th><td>Raw D3</td></tr>
<tr><th scope="row">Connect4</th><td>Raw D3</td></tr>
<tr><th scope="row">Gomoku</th><td><code>div</code>-based</td></tr>
<tr><th scope="row">Grammar Modeling</th><td>Raw D3 &amp; <strong>Default</strong> Graph</td></tr>
<tr><th scope="row"><em>k</em>-Means Clustering</th><td>Z3 Library</td></tr>
<tr><th scope="row">Minesweeper</th><td><code>div</code>-based</td></tr>
<tr><th scope="row">Minesweeper (1)</th><td>Z3 Library</td></tr>
<tr><th scope="row">Minesweeper (2)</th><td>D3FX</td></tr>
<tr><th scope="row">OS Memory Mgmt.</th><td><strong>Default</strong> Graph</td></tr>
<tr><th scope="row">Online Payment Sys.</th><td><strong>Default</strong> Table</td></tr>
<tr><th scope="row">Polyomino Packing</th><td>Z3 Library</td></tr>
<tr><th scope="row">RPG Randomizer</th><td><strong>Default</strong> Graph</td></tr>
<tr><th scope="row">Runway Traffic</th><td><code>div</code>-based</td></tr>
<tr><th scope="row">Rust Lifetimes</th><td>Raw D3</td></tr>
<tr><th scope="row">Skyscrapers</th><td>Raw D3</td></tr>
<tr><th scope="row">Spikeball</th><td>D3FX</td></tr>
<tr><th scope="row">Sudoku</th><td>Raw D3</td></tr>
<tr><th scope="row">TA Queue</th><td><code>div</code>-based</td></tr>
<tr><th scope="row">Texas Hold’em</th><td><code>div</code>-based</td></tr>
<tr><th scope="row">Triple Triad</th><td><code>div</code>-based</td></tr>
<tr><th scope="row">Uno</th><td>D3FX</td></tr>
</tbody>
</table>
    </div>
    <div class="figshots">
    <figure class="subfig">
      <button type="button" class="zoom" data-full="images/img-021-027.png" aria-label="Enlarge (a) Spikeball (D3FX)"><img src="images/img-021-027.png" alt="A Spikeball game state: a grid of coloured player tokens beside a panel of per-team scores and touches." loading="lazy"></button>
      <figcaption>(a) Spikeball (D3FX)</figcaption>
    </figure>
    <figure class="subfig">
      <button type="button" class="zoom" data-full="images/img-021-029.png" aria-label="Enlarge (b) Uno (D3FX) and Triple Triad (div-based)"><img src="images/img-021-029.png" alt="Two visualisations side by side: an Uno hand of coloured number cards, and a Triple Triad board of numbered tiles." loading="lazy"></button>
      <figcaption>(b) Uno (D3FX) and Triple Triad (<code>div</code>-based)</figcaption>
    </figure>
    <figure class="subfig">
      <button type="button" class="zoom" data-full="images/img-021-033.png" aria-label="Enlarge (c) Texas Hold’em (div-based)"><img src="images/img-021-033.png" alt="A Texas Hold’em table showing two players' hands and the community cards." loading="lazy"></button>
      <figcaption>(c) Texas Hold’em (<code>div</code>-based)</figcaption>
    </figure>
    </div>
  </div>
  <figcaption><b>Figure 11.</b> Showcase of 2023 final projects. Left: Project titles and visualization modes. Right: Examples of D3FX and <code>div</code>-based-based visualizations. Images used with permission from Noah Atanda, Madison Lease, and Priyanka Solanky (Uno); Michael Donoso, Haley Flores, and Yishan Liu (Spikeball); Nick Bottone, Sebastien Jean-Pierre, and Robert Murray (Triple Triad); and Matthew Boranian and Austin Lang (Texas Hold’em).</figcaption>
</figure>
<p>borrowing in Rust that needed fine-grained control for overlapping colored regions (fig. <a href="#fig10">10</a>), which D3FX did not provide. The final 6 groups (labeled as <code>div</code>-based) created their custom visualizations by manipulating the Sterling page directly. These were adapted from a staff-provided example.</p>
<p>For the midterm, there were more groups (because the project teams were smaller) and fewer groups made custom visualizations. There were 32 groups and 11 made visualizations: 3 of these used D3FX, 4 used Raw D3, and 4 a <code>div</code>-based visualizer. Required reflection surveys for both projects generally confirmed the list of features from 2022, except for one group that wanted to create animations, which our helper library did not support.</p>
<h3 id="sec7.3"><span class="num">7.3</span> Formative Evaluation: Testing</h3>
<p>In the Spring of 2023, we gathered formative data to answer three questions: RQ1. How did students use the ability to write tests that query a correct (<em>wheat</em>) solution? RQ2. What difficulties or frustrations did students experience around querying correct solutions? RQ3. To what extent did students use each of the Forge testing constructs? We do not claim to measure learning efficacy or even to fully answer the above questions. Rather, our aim in this section is to give an initial report on issues found to drive further development. Indeed, we found several issues with how students used testing constructs, in particular the assertions.</p>
<p><em>Experimental Setup.</em> We provided students with hidden, known-correct (wheat) solutions for 2 homework assignments: <span class="sc">river</span> (three river-crossing logic puzzles) and <span class="sc">memory</span> (two algorithms for automated memory management). Students were able to switch between running tests on their own model and running them versus the wheat solution. Our use of wheats is guided by prior work on Examplar [<a href="#ref67" id="cite81" role="doc-biblioref">Wrenn 2022</a>] with one notable departure: we supplied only one wheat because, from our perspective, models are not overconstrained by implementation details in the same way that programs are [<a href="#ref65" id="cite82" role="doc-biblioref">Wrenn et al. 2018</a>]. We also examined patterns of testing in students’ midterm (<span class="sc">mid</span>) and final project (<span class="sc">fin</span>) submissions, since on projects students neither had access to wheats nor any specific guidance on testing beyond the expectation that they test.</p>
<p>Forge provides an <em>opt-in</em> mechanism for logging models, test files, and solver results. Fewer than <span class="sc">20</span> students opted in for <span class="sc">river</span> and <span class="sc">memory</span>; for these, we collected information on how they queried the wheat. This let us observe work-in-progress attempts at testing. However, due to the opt-in nature of logging (which we implemented out of respect for students’ privacy), we have no guarantee that they kept logging enabled consistently. Moreover, this view is shallow: we have no insight into how students reacted to the feedback from the system, only the details of their next query (if any).</p>
<h4 id="sec7.3.1"><span class="num">7.3.1</span> RQ1: Use of Wheats.</h4>
<p>Roughly 90% of students’ submissions for river and memory referenced the wheat. Logs contained 760 runs for <span class="sc">river</span> and 1168 runs for <span class="sc">memory</span> where student tests disagreed with the wheat. On <span class="sc">river</span>, most wheat-failing tests were examples, not assertions (144 assertions, 19%). In contrast, students wrote many assertions for <span class="sc">memory</span> (894 assertions, 77%).</p>
<p><em>Interpretation.</em> The data show that students did use the wheat to check their understanding of the problem. Our data suggest that wheat use is common. However, students who opted out of logging have used wheats differently. We believe that the increase in <code>assert</code> use between <span class="sc">river</span> and <span class="sc">memory</span> is due to the course’s evolution from tests to properties, which are naturally expressed as assertions rather than examples.</p>
<h4 id="sec7.3.2"><span class="num">7.3.2</span> RQ2: Wheat Frustrations.</h4>
<p>For both river and memory, we encouraged students to submit critiques when they believed the wheat was flawed. This both supported students’ thinking critically about modeling choices and gave us visibility into unexpected complications. We received 10 responses for <span class="sc">river</span> and 5 responses for <span class="sc">memory</span>. As a representative example, the river-crossing puzzles in <span class="sc">river</span> involved using a flashlight or boat, sometimes under a time limit. Students wrote and tested a predicate for well-formed states. Reports revealed:</p>
<ul>
  <li>Some students were surprised that the wheat allowed a <em>negative</em> timer value. This was deliberate, since Forge integers overflow. The report prompted a review of the topic.</li>
  <li>Questions were raised about whether a <em>solution</em> state predicate needed to use the location of the flashlight at all, given that the win condition was entirely in terms of people crossing. This was a good critique of our wheat, which was arguably over-constrained.</li>
</ul>
<p><em>Interpretation.</em> While wheats sometimes reinforce core concepts, they can also put artificial restrictions on students. Because a major goal of these assignments is giving students practice with breaking down and specifying properties, providing an exact breakdown in the handout would be self-defeating. Yet, casting the wheat as a <em>unique</em> correct solution is often not appropriate—as <a href="#ref67" id="cite83" role="doc-biblioref">Wrenn</a> [<a href="#ref67" id="cite84" role="doc-biblioref">2022</a>] notes for programming. It is also vital that a wheat not <em>over</em> -constrain. One way to</p>
<figure id="fig12">
  <table>
<thead>
<tr><td></td><th scope="colgroup" colspan="4"># projects using constructs</th><th scope="colgroup" colspan="4">avg(median) uses of constructs</th></tr>
<tr><td></td><th scope="col"><span class="sc">mid</span></th><th scope="col"><span class="sc">fin</span></th><th scope="col"><span class="sc">river</span></th><th scope="col"><span class="sc">memory</span></th><th scope="col"><span class="sc">mid</span></th><th scope="col"><span class="sc">fin</span></th><th scope="col"><span class="sc">river</span></th><th scope="col"><span class="sc">memory</span></th></tr>
</thead>
<tbody>
<tr><th scope="row">total # submissions</th><td>32</td><td>26</td><td>62</td><td>59</td><td></td><td></td><td></td><td></td></tr>
<tr><th scope="row">w/ <code>test suite</code></th><td>19</td><td>20</td><td>N/A</td><td>N/A</td><td>N/A</td><td>N/A</td><td>N/A</td><td>N/A</td></tr>
<tr><th scope="row">w/ <code>test expect</code></th><td>19</td><td>20</td><td>1</td><td>84</td><td>5 (6)</td><td>14 (8)</td><td>0 (0)</td><td>4 (4)</td></tr>
<tr><th scope="row">w/ <code>example</code></th><td>30</td><td>7</td><td>62</td><td>55</td><td>21 (18)</td><td>21 (15)</td><td>19 (13)</td><td>8 (6)</td></tr>
<tr><th scope="row">w/ <code>necessary</code></th><td>2</td><td>2</td><td>6</td><td>14</td><td>2 (1)</td><td>1 (1)</td><td>8 (7)</td><td>5 (5)</td></tr>
<tr><th scope="row">w/ <code>sufficient</code></th><td>0</td><td>0</td><td>4</td><td>15</td><td>1 (1)</td><td>0 (0)</td><td>8 (7)</td><td>5 (5)</td></tr>
</tbody>
</table>
  <figcaption><b>Figure 12.</b> 2023 Forge testing by assignment. Because students were given a stencil for river and memory that contained suite blocks for each predicate, those assignments cannot be used to measure test-suite adoption.</figcaption>
</figure>
<p>address these issues is through trial-and-error debugging. Developing systematic methods is an important topic for future work.</p>
<h4 id="sec7.3.3"><span class="num">7.3.3</span> RQ3: How Did Students Write Tests?</h4>
<p>Figure <a href="#fig12">12</a> reports how many groups used each testing construct and <em>how many tests they wrote</em> with each construct on <span class="sc">river</span>, <span class="sc">memory</span>, the midterm (<span class="sc">mid</span>), and the final (<span class="sc">fin</span>). On the <span class="sc">river</span> and <span class="sc">memory</span> assignments, students were required to write some tests using assertions. They went beyond the requirements to write more examples, but generally did the minimum with all other constructs. <span class="sc">river</span> and <span class="sc">memory</span> required students to write their tests in a separate file; fig. <a href="#fig12">12</a> includes only these tests to avoid double-counting or misjudging student intent. Although students were told to do some testing on the projects, we did not mandate use of <code>example</code>, <code>test expect</code>, <code>test suite</code>, etc. Most groups used <code>test expect</code> extensively. The <code>example</code> construct was common on the midterm but not the final.</p>
<p><em>Interpretation.</em> Students used examples heavily on <span class="sc">river</span> and <span class="sc">memory</span>; <span class="sc">river</span> prompted them to do so. Students tended to favor <code>test expect</code> far more on their midterm and final projects; in the latter case, it may be because <code>example</code> was unsupported in Temporal Forge—yet more than half of groups used <code>test expect</code> on the midterm, before Temporal Forge was introduced. There is clear value to the flexible form, especially when models are complex and examples are onerous to write. With a better interface (section <a href="#sec9">9</a>), we expect more examples. In contrast, students did not use <code>necessary</code> and <code>sufficient</code> assertions on their projects; those forms were clearly unwieldy.</p>
<h2 id="sec8"><span class="num">8</span> Related Work</h2>
<p>Forge is based on Alloy 6 and the Pardinus [<a href="#ref44" id="cite85" role="doc-biblioref">Macedo et al. 2022</a>] engine. The temporal features in Alloy 6 were first developed in the Electrum tool [<a href="#ref45" id="cite86" role="doc-biblioref">Macedo et al. 2016</a>]. Forge differentiates itself from these though its support for language levels (section <a href="#sec3">3</a>), custom visualizations (section <a href="#sec4">4</a>), and broader testing constructs (section <a href="#sec5">5</a>). Sterling [<a href="#ref24" id="cite87" role="doc-biblioref">Dyer 2020</a>] is the foundation for Forge’s visualizations, but with extensions prompted by our formative experiment in 2022 (section <a href="#sec7.2">7.2</a>).</p>
<p>Language levels are not new, especially for teaching [<a href="#ref23" id="cite88" role="doc-biblioref">du Boulay et al. 1999</a>; <a href="#ref28" id="cite89" role="doc-biblioref">Felleisen et al. 2001</a>; <a href="#ref31" id="cite90" role="doc-biblioref">Findler et al. 2002</a>; <a href="#ref32" id="cite91" role="doc-biblioref">Gilsing et al. 2022</a>; <a href="#ref35" id="cite92" role="doc-biblioref">Holt and Wortman 1974</a>; <a href="#ref37" id="cite93" role="doc-biblioref">Homer et al. 2014</a>]. Likewise, others have integrated Racket and solvers—e.g., Rosette [<a href="#ref60" id="cite94" role="doc-biblioref">Torlak and Bodik 2014</a>], a tool for building solver-aided languages. <a href="#ref5" id="cite95" role="doc-biblioref">Andersen et al.</a> [<a href="#ref5" id="cite96" role="doc-biblioref">2020</a>] extend Racket with live, domain-specific <span class="sc">ide</span>s. These efforts are either unrelated to <span class="sc">fm</span>, neglect issues like visualization, or do not focus on pedagogy.</p>
<p>Many others have worked on visualization in Alloy. A representative sample of this work includes magic layout [<a href="#ref54" id="cite97" role="doc-biblioref">Rayside et al. 2007</a>], the visualizer for DynAlloy [<a href="#ref9" id="cite98" role="doc-biblioref">Bendersky et al. 2013</a>; <a href="#ref55" id="cite99" role="doc-biblioref">Regis et al. 2017</a>], and the Web-based visualizer in Alloy4Fun [<a href="#ref46" id="cite101" role="doc-biblioref">Macedo et al. 2021</a>]. <a href="#ref17" id="cite102" role="doc-biblioref">Couto et al.</a> [<a href="#ref17" id="cite103" role="doc-biblioref">2018</a>] propose a broader range of potential layout options for Alloy, including grids and linear orderings. None of these works enable a truly <em>custom</em> visualization like those seen in section 4. Only Alloy4Fun is based on data from a live course.</p>
<p>The full Forge system most closely resembles the excellent yet little known and, we would argue, under-recognized GUPU pedagogic Prolog system [<a href="#ref50" id="cite104" role="doc-biblioref">Neumerkel and Kral 2002</a>; <a href="#ref51" id="cite105" role="doc-biblioref">Neumerkel et al. 1997</a>]. GUPU presents students with a fragment of Prolog and modified syntax that were built with teaching in mind, along with testing capabilities and “viewers” that translate answer substitutions to graphical form. GUPU even allows students to query a hidden solution and gives tailored feedback based on their tests. The main difference lies in the language: GUPU focuses on <em>one</em> sublanguage for declarative <em>programming</em>, whereas Forge gives a <em>progression</em> of languages for lightweight <em>modeling</em> atop a platform that enables domain-specific modeling languages. Another interesting difference is that in GUPU, viewers are themselves written in Prolog, whereas in Forge, they are written in JavaScript (section <a href="#sec9">9</a>). It is unclear which approach is better, although some of our students noted JavaScript as a barrier (section <a href="#sec7.2.4">7.2.4</a>).</p>
<p>AT(P) [<a href="#ref7" id="cite107" role="doc-biblioref">Beierle et al. 2004a</a>] provides a rich set of testing constructs for Prolog, as well as automated assessment and feedback on preliminary tests. AT(P) includes analogues to <code>example</code>, <code>necessary</code>, etc. but also forms that Forge does not currently support, such as solution counting. AT(P) does not provide a progression of languages or custom visualization, although the underlying framework [<a href="#ref6" id="cite108" role="doc-biblioref">Beierle et al. 2003</a>, <a href="#ref8" id="cite109" role="doc-biblioref">2004b</a>], can support other languages (e.g., Scheme).</p>
<p>AUnit [<a href="#ref59" id="cite110" role="doc-biblioref">Sullivan et al. 2018</a>] extends Alloy with structured testing and related features such as fault localization [<a href="#ref63" id="cite111" role="doc-biblioref">Wang et al. 2020</a>] and automated repair [<a href="#ref62" id="cite112" role="doc-biblioref">Wang et al. 2018</a>]. AUnit separates tests from other commands and supports examples, resolving some of our critiques in section 5. However, AUnit does not enable running tests versus hidden known-good models, which means it is not an immediate fit for our needs. Alloy4Fun [<a href="#ref46" id="cite113" role="doc-biblioref">Macedo et al. 2021</a>] supports “challenges” where students attempt to match a hidden predicate. In contrast, wheats (section <a href="#sec5.2">5.2</a>) are meant to help detect conceptual issues on larger assignments.</p>
<h2 id="sec9"><span class="num">9</span> Discussion</h2>
<p>We close with a few general observations and a list of planned future directions for Forge.</p>
<p><em>Key Takeaways.</em> From a linguistic point of view, we believe there are two key principles to take away from this work:</p>
<ol>
  <li>In general, decompose your complex language into a sequence of increasingly sophisticated layers. We believe this principle can apply to many languages used in formal methods, which have a variety of complex operators, clever shorthands, and so on. These features are valuable to experts but can be confusing to beginners.</li>
  <li>In the context of relational modeling languages such as Alloy, consider starting with functional specifications and delaying relational (and temporal) operators until students have basic skills and are ready for problems that motivate these operators.</li>
</ol>
<p>From a presentation perspective, we believe the evidence shown for custom visualizations—in terms of highlighting salient information (figs. <a href="#fig4">4</a> and <a href="#fig6">6</a>), reducing clutter (figs. <a href="#fig4">4</a> and <a href="#fig6">6</a>), and avoiding outright confusion that might almost be considered misinformation (fig. <a href="#fig5">5</a>)—is very compelling. Moreover, because Sterling is not just Forge-centric (it speaks the same protocol as Alloy and was originally created for Alloy), visualizations created in Sterling are, in principle, usable for instances produced by other tools.</p>
<p>Finally, we believe there is a useful progression from testing to formal methods. This has been discussed more narrowly in prior work, e.g., for property-based testing [<a href="#ref66" id="cite114" role="doc-biblioref">Wrenn et al. 2021</a>]. We believe we have offered some useful guidelines about how to proceed here, and also linked the topic to other work in computing education. However, some care is needed. In regard to testing, this paper is a preliminary effort; a careful treatment is a topic for future work and course offerings.</p>
<p><em>Students and Telemetry.</em> Forge includes an optional telemetry system that collects snapshots of every file submitted to the language for feedback. To opt in, students must replace a default string at the top of their assignment with an anonymous ID. In principle, these IDs let us build a timeline of file snapshots and discover, e.g., how students reacted to a particular error message. However, we have seen increasing reluctance toward logging among both students and course staff. This may be a local issue or part of a larger trend; we merely note it. Students were certainly not shy about leaving (sometimes extensive, often useful) feedback in anonymous surveys.</p>
<p><em>Towards a Testing Recipe.</em> Students struggle with testing their models early in the development process. Even if the tool provides testing features, a methodology is needed. In the programming context, works like <em>How to Design Programs</em> [<a href="#ref28" id="cite115" role="doc-biblioref">Felleisen et al. 2001</a>] equip students with a <em>design</em> <em>recipe</em> so they can proceed systematically toward correct solutions with minimal feedback from course staff. We envision a testing recipe for student models that begins with <code>example</code>s of how each predicate should behave, and eventually evolves into <code>assert</code>s that partially specify a correct solution. In 2023, we taught a variation of this recipe to students, but they did not use it—perhaps because the methodology was tied to running against hidden correct solutions (section <a href="#sec5">5</a>) that were also involved in the grading process. We suspect that a recipe will help students structure their modeling but further work on separating the essential ideas is needed.</p>
<p><em>Instance Examples and Comprehension.</em> Currently, the only way to write examples in Forge is through the coding interface. Students must painstakingly describe object graphs textually (fig. <a href="#fig7">7</a>) A projectional editing interface (e.g.,[<a href="#ref5" id="cite116" role="doc-biblioref">Andersen et al. 2020</a>; <a href="#ref15" id="cite117" role="doc-biblioref">Chugh et al. 2016</a>; <a href="#ref34" id="cite118" role="doc-biblioref">Hempel et al. 2018</a>]) or a graphical interface akin to the one Crucible [<a href="#ref27" id="cite119" role="doc-biblioref">Emerson and Sullivan 2023</a>] provides would eliminate typo-level errors and give students more time to focus on quality tests. Relatedly, since the instances students receive when a test fails (section <a href="#sec5.2">5.2</a>) might be large, it would be useful to categorize the failure, perhaps by leveraging the auto-grading suite for the assignment, and provide hinting in natural language alongside the instance.</p>
<p><em>Domain-Specific Modeling Languages.</em> As mentioned in section <a href="#sec6">6</a>, one can create <em>domain-specific</em> <em>modeling languages</em> that compile into Forge’s core language. By way of example, Forge supports a custom language for writing cryptographic protocols, inspired by the input language of the CPSA [<a href="#ref21" id="cite120" role="doc-biblioref">Doghmi et al. 2007</a>] protocol-analysis tool, and was used to generate the example shown in section 4.1. While many domains do already have powerful formal tools (e.g., [<a href="#ref11" id="cite121" role="doc-biblioref">Blanchet 2016</a>; <a href="#ref21" id="cite122" role="doc-biblioref">Doghmi et al. 2007</a>] for protocols), Forge can provide simplified forms of their languages to give students a quick taste of what <span class="sc">fm</span> can do. We believe there is great value to creating these kinds of domain-specific modeling languages, where students are introduced to <span class="sc">fm</span> through the use of domains that they understand well or care about (whether cryptography or river puzzles or baseball). Combining domain-specific modeling languages with domain-specific visualizations would create an epistemically-closed universe where students can focus on the domain alone, and the general-purpose nature of Forge hides until needed (and never appears, in some settings).</p>
<p><em>Other Future Work.</em> Development on Forge is ongoing. Our evaluation points to numerous areas for improvement, some of which entail a bit of engineering, and others that are research topics in their own right. For example, students objected to mixing singletons and sets in Relational Forge (section <a href="#sec7.1">7.1</a>); what would the consequences be of enforcing further restriction on comparison? Students found Temporal Forge convenient for stateful models; given that relations and temporal operators seem independent, why not offer a Temporal Froglet language level? Priming expressions confused students; what sorts of static checks are possible? Can the lessons from section <a href="#sec7.2">7.2</a> and systems like GUPU [<a href="#ref51" id="cite123" role="doc-biblioref">Neumerkel et al. 1997</a>] lead to a Sterling where students do not need learn JavaScript to write custom visualizations? What is the pedagogic relationship (if any) between language levels and the theories provided by SMT-based tools? Finally, and more generally, we believe that learning modeling, how to precisely express invariants, etc. are valuable for building engineering skills outside of formal methods. However, we have no rigorous evidence for this. A longitudinal study of students in advanced computer-science courses could be informative.</p>
<p>Our ultimate goal is not to fragment the Alloy community. Rather, we hope that insights from our pedagogic context are useful in helping improve both tools. We also plan to incorporate pedagogically-useful additions to Alloy as they appear; for instance, records [<a href="#ref13" id="cite124" role="doc-biblioref">Brunel et al. 2023</a>] could be worthwhile in our setting.</p>
<h2 id="data-availability-statement">Data-Availability Statement</h2>
<p>The Forge tool is Open Source and hosted on a public repository (section <a href="#sec1">1</a>). This paper has an artifact that includes Forge, its documentation, the survey instruments, and all necessary code to support the modelling and visualization examples in the paper [<a href="#ref49" id="cite125" role="doc-biblioref">Nelson et al. 2024</a>].</p>
<h2 id="acknowledgments">Acknowledgments</h2>
<p>We are grateful to the Alloy and Electrum teams for creating excellent tooling we could build on. Our thinking on gradual <span class="sc">fm</span> was profoundly influenced by Daniel Jackson, whom we also thank for numerous thought-provoking conversations. Pamela Zave contributed many useful discussions, including of visualization challenges. Shriram Krishnamurthi thanks Markus Triska for pointing him to GUPU.</p>
<p>We owe a debt to the many students over the past decade who have taken our courses in Alloy and Forge, especially to recent students for their helpful feedback and survey contributions. All project images were used with permission; for this we thank especially Thomas Castleman and Ria Rajesh (Rust); Noah Atanda, Madison Lease, and Priyanka Solanky (Uno); Michael Donoso, Haley Flores, and Yishan Liu (Spikeball); Nick Bottone, Sebastien Jean-Pierre, and Robert Murray (Triple Triad); and Matthew Boranian and Austin Lang (Texas Hold’em). We deeply appreciate other work that students such as Lucy Reyes, Abigail Siegel, Mark Lavrentyev, Emmie He, and others did with Forge while they were at Brown. We particularly thank Anna Ohrt, who worked on enhancements to Forge’s visualizer that will be deployed in the Spring of 2024, but did not yet feature in the tool evaluated here.</p>
<p>We are grateful for support from the US NSF through grants <a href="https://www.nsf.gov/awardsearch/showAward?AWD_ID=2227863&amp;amp;HistoricalAwards=false">SHF-2227863,</a> <a href="https://www.nsf.gov/awardsearch/showAward?AWD_ID=2208731&amp;amp;HistoricalAwards=false">SaTC-2208731,</a> and <a href="https://www.nsf.gov/awardsearch/showAward?AWD_ID=2030859">CCF-2030859.</a> Ben Greenman thanks the CRA for support through the <a href="https://cifellows2020.org">CIFellows</a> project.</p>
<section class="references" id="references">
<h2>References</h2>
<ol>
  <li id="ref1">alloytools.org. 2023. Alloy Analyzer Downloads. <a href="https://alloytools.org/download.html">https://alloytools.org/download.html</a>.Accessed August 27, 2023. <span class="backrefs"><a href="#cite46" aria-label="back to citation">↩</a></span></li>
  <li id="ref2">alloytools.org. 2023a. Case study applications of Alloy. <a href="http://alloytools.org/citations/case-studies.html">http://alloytools.org/citations/case-studies.html</a>.Accessed August 1, 2023. <span class="backrefs"><a href="#cite23" aria-label="back to citation">↩</a></span></li>
  <li id="ref3">alloytools.org. 2023b. Courses using Alloy. <a href="http://alloytools.org/citations/courses.html">http://alloytools.org/citations/courses.html</a>.Accessed August 1, 2023. <span class="backrefs"><a href="#cite25" aria-label="back to citation">↩</a></span></li>
  <li id="ref4">alloytools.org. 2023c. Translation into Alloy. <a href="http://alloytools.org/citations/language-translations.html">http://alloytools.org/citations/language-translations.html</a>.Accessed August 1, 2023. <span class="backrefs"><a href="#cite26" aria-label="back to citation">↩</a></span></li>
  <li id="ref5">Leif Andersen, Michael Ballantyne, and Matthias Felleisen. 2020. Adding Interactive Visual Syntax to Textual Code. PACMPL 4, OOPSLA (2020), 222:1–222:28. <a href="https://doi.org/10.1145/3428290">https://doi.org/10.1145/3428290</a> <span class="backrefs"><a href="#cite95" aria-label="back to citation">↩</a> <a href="#cite96" aria-label="back to citation">↩</a> <a href="#cite116" aria-label="back to citation">↩</a></span></li>
  <li id="ref6">Christoph Beierle, Marjaa Kulaa, and Manfred Widera. 2003. Automatic Analysis of Programming Assignments. In DeLFI. GI, 144–153. <a href="https://dl.gi.de/handle/20.500.12116/15081">https://dl.gi.de/handle/20.500.12116/15081</a> <span class="backrefs"><a href="#cite108" aria-label="back to citation">↩</a></span></li>
  <li id="ref7">Christoph Beierle, Marija Kulaš, and Manfred Widera. 2004a. Partial Specifications of Program Properties. In TeachLP. 17 pages. <a href="https://ep.liu.se/ecp/012/ecp04012.pdf">https://ep.liu.se/ecp/012/ecp04012.pdf</a>.Accessed 2024-01-24. <span class="backrefs"><a href="#cite107" aria-label="back to citation">↩</a></span></li>
  <li id="ref8">Christoph Beierle, Marija Kulaš, and Manfred Widera. 2004b. A Pragmatic Approach to Pre-Testing Prolog Programs. In INAP and WLP. Springer-Verlag, 294–308. <a href="https://doi.org/10.1007/11415763_20">https://doi.org/10.1007/11415763_20</a> <span class="backrefs"><a href="#cite109" aria-label="back to citation">↩</a></span></li>
  <li id="ref9">Pablo Bendersky, Juan Pablo Galeotti, and Diego Garbervetsky. 2013. The DynAlloy Visualizer. In Latin American Workshop on Formal Methods, Vol. 139. 59–64. <a href="https://doi.org/10.4204/EPTCS.139.6">https://doi.org/10.4204/EPTCS.139.6</a> <span class="backrefs"><a href="#cite98" aria-label="back to citation">↩</a></span></li>
  <li id="ref10">Armin Biere, Alessandro Cimatti, Edmund M. Clarke, and Yunshan Zhu. 1999. Symbolic Model Checking without BDDs. In TACAS. Springer, 193–207. <a href="https://doi.org/10.1007/3-540-49059-0_14">https://doi.org/10.1007/3-540-49059-0_14</a> <span class="backrefs"><a href="#cite19" aria-label="back to citation">↩</a></span></li>
  <li id="ref11">Bruno Blanchet. 2016. Modeling and Verifying Security Protocols with the Applied Pi Calculus and ProVerif. Foundations and Trends in Privacy and Security 1, 1–2 (2016), 1–135. <a href="https://doi.org/10.1561/3300000004">https://doi.org/10.1561/3300000004</a> <span class="backrefs"><a href="#cite121" aria-label="back to citation">↩</a></span></li>
  <li id="ref12">Edwin C. Brady. 2013. Idris, A General-Purpose Dependently Typed Programming Language: Design and Implementation. Journal of Functional Programming 23, 5 (2013), 552–593. <a href="https://doi.org/10.1017/S095679681300018X">https://doi.org/10.1017/S095679681300018X</a> <span class="backrefs"><a href="#cite2" aria-label="back to citation">↩</a> <a href="#cite3" aria-label="back to citation">↩</a></span></li>
  <li id="ref13">Julien Brunel, David Chemouil, Alcino Cunha, and Nuno Macedo. 2023. Adding Records to Alloy. In ABZ. Springer, 212–219. <a href="https://doi.org/10.1007/978-3-031-33163-3_16">https://doi.org/10.1007/978-3-031-33163-3_16</a> <span class="backrefs"><a href="#cite124" aria-label="back to citation">↩</a></span></li>
  <li id="ref14">Carlos Caleiro, Luca Viganò, and David Basin. 2006. On the Semantics of Alice&amp;Bob Specifications of Security Protocols. Theoretical Computer Science 367, 1–2 (2006), 88–122. <a href="https://doi.org/10.1016/J.TCS.2006.08.041">https://doi.org/10.1016/J.TCS.2006.08.041</a> <span class="backrefs"><a href="#cite57" aria-label="back to citation">↩</a></span></li>
  <li id="ref15">Ravi Chugh, Brian Hempel, Mitchell Spradlin, and Jacob Albers. 2016. Programmatic and Direct Manipulation, Together at Last. In PLDI. ACM, 341–354. <a href="https://doi.org/10.1145/2908080.2908103">https://doi.org/10.1145/2908080.2908103</a> <span class="backrefs"><a href="#cite117" aria-label="back to citation">↩</a></span></li>
  <li id="ref16">Koen Claessen and John Hughes. 2000. QuickCheck: A Lightweight Tool for Random Testing of Haskell Programs. In ICFP. ACM, 268–279. <a href="https://doi.org/10.1145/357766.351266">https://doi.org/10.1145/357766.351266</a> <span class="backrefs"><a href="#cite4" aria-label="back to citation">↩</a> <a href="#cite5" aria-label="back to citation">↩</a></span></li>
  <li id="ref17">Rui Couto, José Creissac Campos, Nuno Macedo, and Alcino Cunha. 2018. Improving the Visualization of Alloy Instances. In F-IDE@FLoC, Vol. 284. 37–52. <a href="https://doi.org/10.4204/EPTCS.284.4">https://doi.org/10.4204/EPTCS.284.4</a> <span class="backrefs"><a href="#cite102" aria-label="back to citation">↩</a> <a href="#cite103" aria-label="back to citation">↩</a></span></li>
  <li id="ref18">Leonardo de Moura and N. Bjørner. 2008. Z3: An efficient SMT solver. In TACAS. Springer, 337–340. <a href="https://doi.org/10.1007/978-3-540-78800-3_24">https://doi.org/10.1007/978-3-540-78800-3_24</a> <span class="backrefs"><a href="#cite6" aria-label="back to citation">↩</a> <a href="#cite7" aria-label="back to citation">↩</a> <a href="#cite69" aria-label="back to citation">↩</a> <a href="#cite80" aria-label="back to citation">↩</a></span></li>
  <li id="ref19">Greg Dennis, Felix Sheng-Ho Chang, and Daniel Jackson. 2006. Modular Verification of Code with SAT. In ISSTA. ACM, 109–120. <a href="https://doi.org/10.1145/1146238.1146251">https://doi.org/10.1145/1146238.1146251</a> <span class="backrefs"><a href="#cite1" aria-label="back to citation">↩</a></span></li>
  <li id="ref20">Paul Denny, James Prather, Brett A. Becker, Zachary Albrecht, Dastyni Loksa, and Raymond Pettit. 2019. A Closer Look at Metacognitive Scaffolding: Solving Test Cases Before Programming. In Koli Calling. ACM, 11:1–11:10. https: //doi.org/10.1145/3364510.3366170 <span class="backrefs"><a href="#cite61" aria-label="back to citation">↩</a></span></li>
  <li id="ref21">Shaddin F. Doghmi, Joshua D. Guttman, and F. Javier Thayer. 2007. Searching for Shapes in Cryptographic Protocols. In TACAS. Springer, 523–537. <a href="https://doi.org/10.1007/978-3-540-71209-1_41">https://doi.org/10.1007/978-3-540-71209-1_41</a> <span class="backrefs"><a href="#cite120" aria-label="back to citation">↩</a> <a href="#cite122" aria-label="back to citation">↩</a></span></li>
  <li id="ref22">Danny Dolev and Andrew Chi-Chih Yao. 1983. On the Security of Public Key Protocols. IEEE Transactions on Information Theory 29, 2 (1983), 198–207. <a href="https://doi.org/10.1109/TIT.1983.1056650">https://doi.org/10.1109/TIT.1983.1056650</a> <span class="backrefs"><a href="#cite53" aria-label="back to citation">↩</a> <a href="#cite55" aria-label="back to citation">↩</a></span></li>
  <li id="ref23">Benedict du Boulay, Tim O’Shea, and John Monk. 1999. The Black Box Inside the Glass Box. International Journal of Human-Computer Studies 51, 2 (1999), 265–277. <a href="https://doi.org/10.1006/IJHC.1981.0309">https://doi.org/10.1006/IJHC.1981.0309</a> <span class="backrefs"><a href="#cite37" aria-label="back to citation">↩</a> <a href="#cite88" aria-label="back to citation">↩</a></span></li>
  <li id="ref24">Andrew Tristan Dyer. 2020. Lightweight Formal Methods in Scientific Computing. Ph. D. Dissertation. North Carolina State University. <a href="https://repository.lib.ncsu.edu/items/95554653-06ab-4a76-adbd-846f2c9b995f">https://repository.lib.ncsu.edu/items/95554653-06ab-4a76-adbd-846f2c9b995f</a>.Accessed 2024-01-24. <span class="backrefs"><a href="#cite30" aria-label="back to citation">↩</a> <a href="#cite50" aria-label="back to citation">↩</a> <a href="#cite78" aria-label="back to citation">↩</a> <a href="#cite79" aria-label="back to citation">↩</a> <a href="#cite87" aria-label="back to citation">↩</a></span></li>
  <li id="ref25">Tristan Dyer and John Baugh. 2021. Sterling: A Web-Based Visualizer for Relational Modeling Languages. In ABZ. Springer, 99–104. <a href="https://doi.org/10.1007/978-3-030-77543-8_7">https://doi.org/10.1007/978-3-030-77543-8_7</a> <span class="backrefs"><a href="#cite66" aria-label="back to citation">↩</a></span></li>
  <li id="ref26">Jonathan Edwards, Daniel Jackson, and Emina Torlak. 2004. A Type System for Object Models. In FSE. ACM, 189–199. <a href="https://doi.org/10.1145/1029894.1029921">https://doi.org/10.1145/1029894.1029921</a> <span class="backrefs"><a href="#cite44" aria-label="back to citation">↩</a></span></li>
  <li id="ref27">Adam G. Emerson and Allison Sullivan. 2023. Crucible: Graphical Test Cases for Alloy Models. In ISSRE. IEEE, 218–227. <a href="https://doi.org/10.1109/ISSRE59848.2023.00065">https://doi.org/10.1109/ISSRE59848.2023.00065</a> <span class="backrefs"><a href="#cite119" aria-label="back to citation">↩</a></span></li>
  <li id="ref28">Matthias Felleisen, Robert Bruce Findler, Matthew Flatt, and Shriram Krishnamurthi. 2001. How to Design Programs. MIT Press. <a href="http://www.htdp.org/">http://www.htdp.org/</a> <span class="backrefs"><a href="#cite41" aria-label="back to citation">↩</a> <a href="#cite89" aria-label="back to citation">↩</a> <a href="#cite115" aria-label="back to citation">↩</a></span></li>
  <li id="ref29">Matthias Felleisen, Robert Bruce Findler, Matthew Flatt, Shriram Krishnamurthi, Eli Barzilay, Jay McCarthy, and Sam Tobin-Hochstadt. 2018. A Programmable Programming Language. Communications of the ACM 61, 3 (2018), 62–71. <a href="https://doi.org/10.1145/3127323">https://doi.org/10.1145/3127323</a> <span class="backrefs"><a href="#cite31" aria-label="back to citation">↩</a> <a href="#cite49" aria-label="back to citation">↩</a></span></li>
  <li id="ref30">Matthias Felleisen, Robert Bruce Findler, Matthew Flatt, Shriram Krishnamurthi, Eli Barzilay, Jay A. McCarthy, and Sam Tobin-Hochstadt. 2015. The Racket Manifesto. In SNAPL. Schloss Dagstuhl, 113–128. <a href="https://doi.org/10.4230/LIPIcs.SNAPL.2015.113">https://doi.org/10.4230/LIPIcs.SNAPL.2015.113</a> <span class="backrefs"><a href="#cite63" aria-label="back to citation">↩</a></span></li>
  <li id="ref31">Robert Bruce Findler, John Clements, Cormac Flanagan, Matthew Flatt, Shriram Krishnamurthi, Paul Steckler, and Matthias Felleisen. 2002. DrScheme: A Programming Environment for Scheme. Journal of Functional Programming 12, 2 (2002), 159–182. <a href="https://doi.org/10.1017/S0956796801004208">https://doi.org/10.1017/S0956796801004208</a> <span class="backrefs"><a href="#cite28" aria-label="back to citation">↩</a> <a href="#cite39" aria-label="back to citation">↩</a> <a href="#cite45" aria-label="back to citation">↩</a> <a href="#cite90" aria-label="back to citation">↩</a></span></li>
  <li id="ref32">Marleen Gilsing, Jesús Pelay, and Felienne Hermans. 2022. Design, Implementation and Evaluation of the Hedy Programming Language. Journal of Computer Languages 73, 101158 (2022), 17 pages. <a href="https://doi.org/10.1016/J.COLA.2022.101158">https://doi.org/10.1016/J.COLA.2022.101158</a> <span class="backrefs"><a href="#cite91" aria-label="back to citation">↩</a></span></li>
  <li id="ref33">Ben Greenman, Sam Saarinen, Tim Nelson, and Shriram Krishnamurthi. 2023. Little Tricky Logic: Misconceptions in the Understanding of LTL. Programming 7, 2 (2023), 7:1–7:37. <a href="https://doi.org/10.22152/programming-journal.org/2023/7/7">https://doi.org/10.22152/programming-journal.org/2023/7/7</a> <span class="backrefs"><a href="#cite72" aria-label="back to citation">↩</a> <a href="#cite73" aria-label="back to citation">↩</a> <a href="#cite76" aria-label="back to citation">↩</a> <a href="#cite77" aria-label="back to citation">↩</a></span></li>
  <li id="ref34">Brian Hempel, Justin Lubin, Grace Lu, and Ravi Chugh. 2018. Deuce: A Lightweight User Interface for Structured Editing. In ICSE. ACM, 654–664. <a href="https://doi.org/10.1145/3180155.3180165">https://doi.org/10.1145/3180155.3180165</a> <span class="backrefs"><a href="#cite118" aria-label="back to citation">↩</a></span></li>
  <li id="ref35">Richard C. Holt and David B. Wortman. 1974. A Sequence of Structured Subsets of PL/I. In SIGCSE. ACM, 129–132. <a href="https://doi.org/10.1145/800183.810456">https://doi.org/10.1145/800183.810456</a> <span class="backrefs"><a href="#cite40" aria-label="back to citation">↩</a> <a href="#cite92" aria-label="back to citation">↩</a></span></li>
  <li id="ref36">Gerard J. Holzmann. 2003. The Spin Model Checker: Primer and Reference Manual. Addison-Wesley. <a href="https://doi.org/10.5555/2029108">https://doi.org/10.5555/2029108</a> <span class="backrefs"><a href="#cite8" aria-label="back to citation">↩</a> <a href="#cite9" aria-label="back to citation">↩</a></span></li>
  <li id="ref37">Michael Homer, Timothy Jones, James Noble, Kim B. Bruce, and Andrew P. Black. 2014. Graceful Dialects. In ECOOP. Springer, 131–156. <a href="https://doi.org/10.1007/978-3-662-44202-9_6">https://doi.org/10.1007/978-3-662-44202-9_6</a> <span class="backrefs"><a href="#cite42" aria-label="back to citation">↩</a> <a href="#cite93" aria-label="back to citation">↩</a></span></li>
  <li id="ref38">Daniel Jackson. 2002. Alloy: A Lightweight Object Modelling Notation. ACM Transactions on Software Engineering and Methodology 11, 2 (2002), 256–290. <a href="https://doi.org/10.1145/505145.505149">https://doi.org/10.1145/505145.505149</a> <span class="backrefs"><a href="#cite17" aria-label="back to citation">↩</a></span></li>
  <li id="ref39">Daniel Jackson. 2012. Software Abstractions: Logic, Language, and Analysis (2 ed.). MIT Press. <a href="https://doi.org/10.5555/2141100">https://doi.org/10.5555/2141100</a> <span class="backrefs"><a href="#cite14" aria-label="back to citation">↩</a> <a href="#cite35" aria-label="back to citation">↩</a> <a href="#cite36" aria-label="back to citation">↩</a> <a href="#cite43" aria-label="back to citation">↩</a></span></li>
  <li id="ref40">Daniel Jackson. 2019. Alloy: A Language and Tool for Exploring Software Designs. Communications of the ACM 62, 9 (2019), 66–76. <a href="https://doi.org/10.1145/3338843">https://doi.org/10.1145/3338843</a> <span class="backrefs"><a href="#cite27" aria-label="back to citation">↩</a></span></li>
  <li id="ref41">Daniel Jackson and Jeanette Wing. 1996. Lightweight Formal Methods. IEEE Computer (1996). <a href="https://people.csail.mit.edu/dnj/publications/ieee96-roundtable.html">https://people.csail.mit.edu/dnj/publications/ieee96-roundtable.html</a>. Accessed 2024-01-24. <span class="backrefs"><a href="#cite15" aria-label="back to citation">↩</a> <a href="#cite16" aria-label="back to citation">↩</a> <a href="#cite33" aria-label="back to citation">↩</a> <a href="#cite34" aria-label="back to citation">↩</a></span></li>
  <li id="ref42">William Jernigan, Amber Horvath, Michael Lee, Margaret Burnett, Taylor Cuilty, Sandeep Kuttal, Anicia Peters, Irwin Kwan, Faezeh Bahmani, Amy Ko, Christopher J. Mendez, and Alannah Oleson. 2017. General principles for a Generalized Idea Garden. Journal of Visual Languages and Computing 39 (2017), 51–65. <a href="https://doi.org/10.1016/j.jvlc.2017.04.005">https://doi.org/10.1016/j.jvlc.2017.04.005</a> <span class="backrefs"><a href="#cite22" aria-label="back to citation">↩</a></span></li>
  <li id="ref43">K. Rustan M. Leino. 2010. Dafny: An Automatic Program Verifier for Functional Correctness. In LPAR. Springer, 348–370. <a href="https://doi.org/10.1007/978-3-642-17511-4_20">https://doi.org/10.1007/978-3-642-17511-4_20</a> <span class="backrefs"><a href="#cite10" aria-label="back to citation">↩</a> <a href="#cite11" aria-label="back to citation">↩</a></span></li>
  <li id="ref44">Nuno Macedo, Julien Brunel, David Chemouil, and Alcino Cunha. 2022. Pardinus: A Temporal Relational Model Finder. Journal of Automated Reasoning 66, 4 (2022), 861–904. <a href="https://doi.org/10.1007/s10817-022-09642-2">https://doi.org/10.1007/s10817-022-09642-2</a> <span class="backrefs"><a href="#cite64" aria-label="back to citation">↩</a> <a href="#cite85" aria-label="back to citation">↩</a></span></li>
  <li id="ref45">Nuno Macedo, Julien Brunel, David Chemouil, Alcino Cunha, and Denis Kuperberg. 2016. Lightweight Specification and Analysis of Dynamic Systems with Rich Configurations. In FSE. ACM, 373–383. <a href="https://doi.org/10.1145/2950290.2950318">https://doi.org/10.1145/2950290.2950318</a> <span class="backrefs"><a href="#cite48" aria-label="back to citation">↩</a> <a href="#cite86" aria-label="back to citation">↩</a></span></li>
  <li id="ref46">Nuno Macedo, Alcino Cunha, José Pereira, Renato Carvalho, Ricardo Silva, Ana C. R. Paiva, Miguel Sozinho Ramalho, and Daniel Castro Silva. 2021. Experiences on Teaching Alloy with an Automated Assessment Platform. Science of Computer Programming 211, 102690 (2021), 21 pages. <a href="https://doi.org/10.1016/j.scico.2021.102690">https://doi.org/10.1016/j.scico.2021.102690</a> <span class="backrefs"><a href="#cite101" aria-label="back to citation">↩</a> <a href="#cite113" aria-label="back to citation">↩</a></span></li>
  <li id="ref47">Jay McCarthy and Shriram Krishnamurthi. 2008. Cryptographic Protocol Explication and End-Point Projection. In ESORICS. Springer, 533–547. <a href="https://doi.org/10.1007/978-3-540-88313-5_34">https://doi.org/10.1007/978-3-540-88313-5_34</a> <span class="backrefs"><a href="#cite58" aria-label="back to citation">↩</a></span></li>
  <li id="ref48">Vajih Montaghami and Derek Rayside. 2012. Extending Alloy with Partial Instances. In ABZ. Springer, 122–135. https: //doi.org/10.1007/978-3-642-30885-7_9 <span class="backrefs"><a href="#cite67" aria-label="back to citation">↩</a> <a href="#cite68" aria-label="back to citation">↩</a></span></li>
  <li id="ref49">Tim Nelson, Ben Greenman, Siddhartha Prasad, Tristan Dyer, Ethan Bove, Qianfan Chen, Charles Cutting, Thomas Del Vecchio, Sidney LeVine, Julianne Rudner, Benjamin Ryjikov, Alexander Varga, Andrew Wagner, Luke West, and Shriram Krishnamurthi. 2024. Artifact for Forge: A Tool and Language for Teaching Formal Methods. <a href="https://doi.org/10.5281/zenodo.10463960">https://doi.org/10.5281/zenodo.10463960</a> <span class="backrefs"><a href="#cite32" aria-label="back to citation">↩</a> <a href="#cite125" aria-label="back to citation">↩</a></span></li>
  <li id="ref50">Ulrich Neumerkel and Stefan Kral. 2002. Declarative Program Development in Prolog with GUPU. In WLPE. 77–86. <a href="https://arxiv.org/abs/cs/0207044">https://arxiv.org/abs/cs/0207044</a> <span class="backrefs"><a href="#cite104" aria-label="back to citation">↩</a></span></li>
  <li id="ref51">Ulrich Neumerkel, Christoph Rettig, and Christian Schallart. 1997. Visualizing Solutions with Viewers. In LPE. 43–50. <a href="https://www.complang.tuwien.ac.at/ulrich/papers/PDF/wlpe97.pdf">https://www.complang.tuwien.ac.at/ulrich/papers/PDF/wlpe97.pdf</a>.Accessed 2024-01-24. <span class="backrefs"><a href="#cite105" aria-label="back to citation">↩</a> <a href="#cite123" aria-label="back to citation">↩</a></span></li>
  <li id="ref52">Tobias Nipkow, Markus Wenzel, and Lawrence C. Paulson. 2002. Isabelle/HOL: A Proof Assistant for Higher-Order Logic. Springer-Verlag. <a href="https://doi.org/10.1007/3-540-45949-9">https://doi.org/10.1007/3-540-45949-9</a> <span class="backrefs"><a href="#cite12" aria-label="back to citation">↩</a> <a href="#cite13" aria-label="back to citation">↩</a></span></li>
  <li id="ref53">Observable. 2023. D3: Data-Driven Documents. <a href="https://d3js.org">https://d3js.org</a>.Accessed August 25, 2023. <span class="backrefs"><a href="#cite51" aria-label="back to citation">↩</a></span></li>
  <li id="ref54">Derek Rayside, Felix Sheng-Ho Chang, Greg Dennis, Robert Seater, and Daniel Jackson. 2007. Automatic Visualization of Relational Logic Models. Electronic Communications of the EASST 7 (2007), 15 pages. <a href="https://doi.org/10.14279/tuj.eceasst.7.94">https://doi.org/10.14279/tuj.eceasst.7.94</a> <span class="backrefs"><a href="#cite97" aria-label="back to citation">↩</a></span></li>
  <li id="ref55">Germán Regis, César Cornejo, Simón Gutiérrez Brida, Mariano Politano, Fernando Raverta, Pablo Ponzio, Nazareno Aguirre, Juan Pablo Galeotti, and Marcelo Frias. 2017. DynAlloy Analyzer: A Tool for the Specification and Analysis of Alloy Models with Dynamic Behaviour. In FSE. ACM, 969–973. <a href="https://doi.org/10.1145/3106237.3122826">https://doi.org/10.1145/3106237.3122826</a> <span class="backrefs"><a href="#cite99" aria-label="back to citation">↩</a></span></li>
  <li id="ref56">Sam Saarinen. 2021. Query Strategies for Directed Graphical Models and their Application to Adaptive Testing. Ph. D. Dissertation. Brown University. <a href="https://repository.library.brown.edu/studio/item/bdr:kgyft3b4/">https://repository.library.brown.edu/studio/item/bdr:kgyft3b4/</a> <span class="backrefs"><a href="#cite74" aria-label="back to citation">↩</a> <a href="#cite75" aria-label="back to citation">↩</a></span></li>
  <li id="ref57">Abigail Siegel, Mia Santomauro, Tristan Dyer, Tim Nelson, and Shriram Krishnamurthi. 2021. Prototyping Formal Methods Tools: A Protocol Analysis Case Study. In Protocols, Strands, and Logic. Springer, 394–413. <a href="https://doi.org/10.1007/978-3-030-91631-2_22">https://doi.org/10.1007/978-3-030-91631-2_22</a> <span class="backrefs"><a href="#cite56" aria-label="back to citation">↩</a></span></li>
  <li id="ref58">J. Michael Spivey. 1992. Z Notation — A Reference Manual (2nd ed.). Prentice Hall. <span class="backrefs"><a href="#cite18" aria-label="back to citation">↩</a></span></li>
  <li id="ref59">Allison Sullivan, Kaiyuan Wang, and Sarfraz Khurshid. 2018. AUnit: A Test Automation Tool for Alloy. In ICST. IEEE, 398–403. <a href="https://doi.org/10.1109/ICST.2018.00047">https://doi.org/10.1109/ICST.2018.00047</a> <span class="backrefs"><a href="#cite60" aria-label="back to citation">↩</a> <a href="#cite110" aria-label="back to citation">↩</a></span></li>
  <li id="ref60">Emina Torlak and Rastislav Bodik. 2014. A Lightweight Symbolic Virtual Machine for Solver-Aided Host Languages. In PLDI. ACM, 530–541. <a href="https://doi.org/10.1145/2594291.2594340">https://doi.org/10.1145/2594291.2594340</a> <span class="backrefs"><a href="#cite94" aria-label="back to citation">↩</a></span></li>
  <li id="ref61">Preston Tunnell Wilson, Ben Greenman, Justin Pombrio, and Shriram Krishnamurthi. 2018. The Behavior of Gradual Types: a User Study. In DLS. ACM, 1–12. <a href="https://doi.org/10.1145/3276945.3276947">https://doi.org/10.1145/3276945.3276947</a> <span class="backrefs"><a href="#cite70" aria-label="back to citation">↩</a> <a href="#cite71" aria-label="back to citation">↩</a></span></li>
  <li id="ref62">Kaiyuan Wang, Allison Sullivan, and Sarfraz Khurshid. 2018. Automated Model Repair for Alloy. In ASE. ACM, 577–588. <a href="https://doi.org/10.1145/3238147.3238162">https://doi.org/10.1145/3238147.3238162</a> <span class="backrefs"><a href="#cite112" aria-label="back to citation">↩</a></span></li>
  <li id="ref63">Kaiyuan Wang, Allison Sullivan, Darko Marinov, and Sarfraz Khurshid. 2020. Fault Localization for Declarative Models in Alloy. In ISSRE. IEEE, 391–402. <a href="https://doi.org/10.1109/ISSRE5003.2020.00044">https://doi.org/10.1109/ISSRE5003.2020.00044</a> <span class="backrefs"><a href="#cite111" aria-label="back to citation">↩</a></span></li>
  <li id="ref64">Aaron Wilson, Margaret Burnett, Laura Beckwith, Orion Granatir, Ledah Casburn, Curtis Cook, Mike Durham, and Gregg Rothermel. 2003. Harnessing Curiosity to Increase Correctness in End-User Programming. In CHI. ACM, 305–312. <a href="https://doi.org/10.1145/642611.642665">https://doi.org/10.1145/642611.642665</a> <span class="backrefs"><a href="#cite20" aria-label="back to citation">↩</a></span></li>
  <li id="ref65">John Wrenn, Shriram Krishnamurthi, and Kathi Fisler. 2018. Who Tests the Testers?. In ICER. ACM, 51–59. https: //doi.org/10.1145/3230977.3230999 <span class="backrefs"><a href="#cite82" aria-label="back to citation">↩</a></span></li>
  <li id="ref66">John Wrenn, Tim Nelson, and Shriram Krishnamurthi. 2021. Using Relational Problems to Teach Property-Based Testing. Programming 5, 2 (2021), 9. <a href="https://doi.org/10.22152/programming-journal.org/2021/5/9">https://doi.org/10.22152/programming-journal.org/2021/5/9</a> <span class="backrefs"><a href="#cite114" aria-label="back to citation">↩</a></span></li>
  <li id="ref67">John Sinclair Wrenn. 2022. Executable Examples: Empowering Students to Hone Their Problem Comprehension. Ph. D. Dissertation. Brown University. <a href="https://cs.brown.edu/research/pubs/theses/phd/2022/wrenn.john.pdf">https://cs.brown.edu/research/pubs/theses/phd/2022/wrenn.john.pdf</a>.Accessed 2024-01- 24. <span class="backrefs"><a href="#cite62" aria-label="back to citation">↩</a> <a href="#cite81" aria-label="back to citation">↩</a> <a href="#cite83" aria-label="back to citation">↩</a> <a href="#cite84" aria-label="back to citation">↩</a></span></li>
  <li id="ref68">Pamela Zave. 2020. Discourse Forum Reply. <a href="https://alloytools.discourse.group/t/visualization-for-alloy-what-do-you-want/111/2">https://alloytools.discourse.group/t/visualization-for-alloy-what-do-you-want/111/2</a>.Accessed August 22, 2023. <span class="backrefs"><a href="#cite52" aria-label="back to citation">↩</a></span></li>
  <li id="ref69">Received 20-OCT-2023; accepted 2024-02-24</li>
</ol>
</section>

<footer class="license">
<p>This is an HTML rendering of &ldquo;Forge: A Tool and Language for Teaching
Formal Methods&rdquo;, <i>Proc. ACM Program. Lang.</i> 8, OOPSLA1, Article 116
(April 2024), by Tim Nelson et al.
&copy; 2024 Copyright held by the owner/author(s).</p>
<p>The article is licensed under a
<a href="https://creativecommons.org/licenses/by/4.0/">Creative Commons
Attribution 4.0 International License</a>, which permits this reproduction.
Authoritative version: <a href="https://doi.org/10.1145/3649833">https://doi.org/10.1145/3649833</a> &middot;
<a href="https://cs.brown.edu/people/sk/Publications/Papers/Published/ngp----forge/paper.pdf">original PDF</a>.</p>
</footer>

<dialog class="lightbox" aria-label="Enlarged figure">
  <button type="button" class="close" aria-label="Close">Close &times;</button>
  <div class="wrap"><img src="data:image/gif;base64,R0lGODlhAQABAAAAACH5BAEKAAEALAAAAAABAAEAAAICTAEAOw==" alt=""></div>
</dialog>
<script>
// Click-to-enlarge.  The extracted images are about three times the size
// the PDF displayed them at, so there is genuine detail to reveal.
// Progressive enhancement: without JS every figure is still a plain <img>.
(function () {
  var dlg = document.querySelector('dialog.lightbox');
  if (!dlg || typeof dlg.showModal !== 'function') return;
  var img = dlg.querySelector('img');
  var opener = null;

  document.addEventListener('click', function (ev) {
    var btn = ev.target.closest('button.zoom');
    if (btn) {
      opener = btn;
      img.src = btn.dataset.full;
      img.alt = btn.querySelector('img').alt;
      dlg.showModal();
      return;
    }
    // clicking the backdrop or the close button dismisses
    if (ev.target === dlg || ev.target.closest('.close')) dlg.close();
  });

  dlg.addEventListener('close', function () {
    img.removeAttribute('src');
    if (opener) { opener.focus(); opener = null; }
  });
})();
</script>
</body>
</html>