Skip to content

Commit

Permalink
setup for 1.1 release
Browse files Browse the repository at this point in the history
  • Loading branch information
hugo committed Jul 22, 2024
1 parent de8fdbd commit 6e58562
Show file tree
Hide file tree
Showing 3 changed files with 19 additions and 2 deletions.
14 changes: 14 additions & 0 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
@@ -1,5 +1,19 @@
# Change Log

## V1.1.0
New welformedness checks and fixes.

### New checks
- Checks wether all variables in the right part of a macro are in the left part or public.
- Checks wether all variable in the right part of an equation are in the left part.
- Provides a quick fix for function names again with editing distance.
- Checks wether built-ins are imported to use corresponding functions or symbols (provides a quick fix to import the right built-in).

### Fixes
- Editing distance is now used to display all close tokens (distance < 3) and not the first one only.
- `diff` is considered as a reserved function symbol so that there is no error while using it.
- Functions with arity 0 may be used without parenthesis.

## V1.0.1
Fix package.json

Expand Down
4 changes: 4 additions & 0 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,10 @@ Features:
- Checks the arity of facts and functions.
- Checks whether a lemma uses free terms.
- Checks whether all facts in the premises of the rules appear in the conclusion of some (other) rule (provides a quick fix by using the closest exisiting fact, based on editing distance).
- Checks wether all variables in the right hand side of a macro are in the left hand side or public.
- Checks wether all variable in the right hand side of an equation are in the left hand side.
- Provides a quick fix for function names (suggestions based on editing distance).
- Checks wether built-ins are imported when encountering corresponding functions or symbols (provides a quick fix to import the right built-in).

This is a subset of the checks performed by Tamarin. For more details on Tamarin's wellformedness checks, see the corresponding [Tamarin Prover manual section](https://tamarin-prover.com/manual/master/book/010_modeling-issues.html).

Expand Down
3 changes: 1 addition & 2 deletions TODO.md
Original file line number Diff line number Diff line change
@@ -1,2 +1 @@
- [] Manage preprocessor #IFDEF
- [] Manage Proof method nodes
- [] Manage preprocessor #IFDEF

0 comments on commit 6e58562

Please sign in to comment.