https://github.com/EasyCrypt/easycrypt
Revision 30bfa950afa3806948c073d3c9ec4468d33ea940 authored by Pierre-Yves Strub on 11 December 2023, 10:58:49 UTC, committed by Pierre-Yves Strub on 05 April 2024, 12:45:45 UTC
This tactic allows to change an expression in a statement by some other expression. When applied, the user has to prove that the two expressions are equal (generalizing over all the program variables) This tactic applies to any program logic. The syntax is: proc change <side?> <codepos> : <form> This tactic is in the TCB. Test plan: - unit test (tests/prochange.ec)
1 parent 4ccf645
Tip revision: 30bfa950afa3806948c073d3c9ec4468d33ea940 authored by Pierre-Yves Strub on 11 December 2023, 10:58:49 UTC
New tactic: "proc change"
New tactic: "proc change"
Tip revision: 30bfa95
File | Mode | Size |
---|---|---|
.github | ||
config | ||
examples | ||
scripts | ||
src | ||
tests | ||
theories | ||
.dir-locals.el | -rw-r--r-- | 285 bytes |
.gitignore | -rw-r--r-- | 132 bytes |
AUTHORS | -rw-r--r-- | 543 bytes |
LICENSE | -rw-r--r-- | 1.2 KB |
Makefile | -rw-r--r-- | 1.5 KB |
README.md | -rw-r--r-- | 8.0 KB |
dune | -rw-r--r-- | 221 bytes |
dune-project | -rw-r--r-- | 450 bytes |
easycrypt.opam | -rw-r--r-- | 1.4 KB |
easycrypt.opam.template | -rw-r--r-- | 834 bytes |
easycrypt.png | -rw-r--r-- | 182.6 KB |
flake.lock | -rw-r--r-- | 6.9 KB |
flake.nix | -rw-r--r-- | 3.0 KB |
![swh spinner](/static/img/swh-spinner.gif)
Computing file changes ...