ClemsonRSRG / RESOLVE

RESOLVE (REusable SOftware Language with VErification) is a specification and programming language designed for verifying correctness of object oriented programs.
https://www.cs.clemson.edu/resolve/
BSD 3-Clause "New" or "Revised" License
24 stars 16 forks source link

Extract Theorem Operators #414

Closed yushan87 closed 1 year ago

yushan87 commented 1 year ago

As we populate the symbol table, we store the operators in each of the mathematical assertions we encounter. This will allow the prover to retrieve this information quickly without having to re-walk the expression.