Skip to content

Commit

Permalink
Patch identifier syntax for IMP-VERIFICATION (#28)
Browse files Browse the repository at this point in the history
For the verification module, add new token syntax to `Id` that avoids
collision with other tokens of the rule syntax.
  • Loading branch information
tothtamas28 authored Nov 11, 2024
1 parent 34ce3d7 commit 9dfab04
Showing 1 changed file with 1 addition and 8 deletions.
9 changes: 1 addition & 8 deletions kimp/k-src/imp-verification.k
Original file line number Diff line number Diff line change
Expand Up @@ -2,14 +2,8 @@ requires "statements.k"

module IMP-VERIFICATION-SYNTAX
imports ID-SYNTAX
imports INT-SYNTAX

syntax Id ::= "$s" [token]
| "$s1" [token]
| "$s2" [token]
| "$n" [token]
| "$m" [token]
| "$k" [token]
syntax Id ::= r"\\$[a-zA-Z0-9\\_]+" [token]
endmodule


Expand All @@ -22,5 +16,4 @@ module IMP-VERIFICATION
rule A >=Int B => B <=Int A [simplification]
rule notBool (A <Int B) => B <=Int A [simplification]
rule notBool (A <=Int B) => B <Int A [simplification]

endmodule

0 comments on commit 9dfab04

Please sign in to comment.