cerc-io/solidity
16
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

Update smtchecker.rst

Browse Source
This commit is contained in:
Simon Tian 2021-07-06 23:24:37 +08:00 committed by GitHub
parent 09578e7e22
commit f0ec3dd6a2
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
docs/smtchecker.rst
View File

@ -15,7 +15,7 @@ difference between what you did (the specification) and how you did it
is what you wanted and that you did not miss any unintended effects of it.
Solidity implements a formal verification approach based on
`SMT <https://en.wikipedia.org/wiki/Satisfiability_modulo_theories>`_ and
`SMT (Satisfiability Modulo Theories) <https://en.wikipedia.org/wiki/Satisfiability_modulo_theories>`_ and
`Horn <https://en.wikipedia.org/wiki/Horn-satisfiability>`_ solving.
The SMTChecker module automatically tries to prove that the code satisfies the
specification given by ``require`` and ``assert`` statements. That is, it considers