cerc-io/solidity
10
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

Merge pull request #11623 from simontianx/develop

Browse Source 
Update smtchecker.rst
This commit is contained in:
Leonardo 2021-07-06 18:15:46 +02:00 committed by GitHub
commit 69233c37bd
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. is what you wanted and that you did not miss any unintended effects of it.
Solidity implements a formal verification approach based on 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. `Horn <https://en.wikipedia.org/wiki/Horn-satisfiability>`_ solving.
The SMTChecker module automatically tries to prove that the code satisfies the The SMTChecker module automatically tries to prove that the code satisfies the
specification given by ``require`` and ``assert`` statements. That is, it considers specification given by ``require`` and ``assert`` statements. That is, it considers