creating:safety

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
Next revision		 Previous revision
creating:safety [2025/09/02 19:25] – Finished first draft with challenges ahelwercreating:safety [2025/11/03 23:16] (current) – Removed extra line of code ahelwer
Line 59: Line 59:
 Iterate through all the spec statements to find them: Iterate through all the spec statements to find them:
  
-<code java [highlight_lines_extra="2,3,4,8,9,10,11,12,13,14,15,16,17,18,19"]>+<code java [highlight_lines_extra="2,3,4,8,9,10,11,12,13,14,15,16,17,18"]>
   private final Interpreter interpreter;   private final Interpreter interpreter;
   private Stmt.OpDef init = null;   private Stmt.OpDef init = null;
Line 68: Line 68:
     this.interpreter = interpreter;     this.interpreter = interpreter;
     for (Stmt unit : spec) {     for (Stmt unit : spec) {
-      if (unit instanceof Stmt.OpDef) { +      if (unit instanceof Stmt.OpDef op) {
-        Stmt.OpDef op = (Stmt.OpDef)unit;+
         switch (op.name.lexeme) {         switch (op.name.lexeme) {
-          case "Init"   : init = op; break; +          case "Init"   -> init = op; 
-          case "Next"   : next = op; break; +          case "Next"   -> next = op; 
-          case "Inv"    : invariants.add(op); break; +          case "Inv"    -> invariants.add(op); 
-          case "TypeOK" : invariants.add(op); break; +          case "TypeOK" -> invariants.add(op); 
-          case "Safety" : invariants.add(op); break;+          case "Safety" -> invariants.add(op);
         }         }
       }       }
  • creating/safety.1756841101.txt.gz
  • Last modified: 2025/09/02 19:25
  • by ahelwer