From ffd60978aa9b53d49b4059ed43a721f5071f0a11 Mon Sep 17 00:00:00 2001 From: Regis Blanc <regwblanc@gmail.com> Date: Fri, 27 Mar 2015 17:39:47 +0100 Subject: [PATCH] fix markup --- doc/intro.rst | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/doc/intro.rst b/doc/intro.rst index fab61d5fe..a3964da4b 100644 --- a/doc/intro.rst +++ b/doc/intro.rst @@ -39,13 +39,13 @@ expression. It attempts to prove it using a combination of an internal algorithm and external automated theorem proving. Leon will return one of the following: -* The postcondition is `valid`. In that case, Leon was able to prove that for **any** +* The postcondition is ``valid``. In that case, Leon was able to prove that for **any** input to the function satisfiying the precondition, the postcondition will always hold. -* The postcondition is `invalid`. It means that Leon disproved the postcondition and +* The postcondition is ``invalid``. It means that Leon disproved the postcondition and that there exists at least one input satisfying the precondition and such that the postcondition does not hold. Leon will always return a concrete counterexample, very useful when trying to understand why a function is not satisfying its contract. -* The postcondition is `unknown`. It means Leon is unable to prove or find a counterexample. +* The postcondition is ``unknown``. It means Leon is unable to prove or find a counterexample. It usually happens after a timeout or an internal error occuring in the external theorem prover. -- GitLab