TLA+ logic

[Ron Pressler]

I've seen it mentioned (both by Leslie Lamport and Stephan Merz) that TLA+ is a first order logic. However, it is trivial to write expressions like:

   ∃ epsilon ∈ [SUBSET S → S] : ∀x ∈ SUBSET S : x ≠ {} ⇒ epsilon[x] ∈ x

or even the non-TLC-supported (but perhaps TLAPS-supported?)

    ∃ epsilon : ∀x : x ≠ {} ⇒ epsilon[x] ∈ x

So the ability to quantify over functions, plus the SUBSET and UNION operators (as well as the analogous INTERSECTION operator, easily defined with a set comprehension) “feel” very much second-order. I understand that quantifying over functions is formally an “encoding” of operators in ZF, but is there an actual difference between the expressivity of TLA+ and second (and higher) -order logic?

Ron

[fl]

 

 

 

> So the ability to quantify over functions, plus the SUBSET and UNION operators (as well as the analogous

> INTERSECTION operator, easily defined with a set comprehension) “feel” very much second-order.

Don't forget that in ZFC a function is a class of pairs. It is possible to quantify over functions (and relations)

as long as they are not proper classes.

If you have doubt about that see Metamath.

 

http://us2.metamath.org:88/mpegif/mmrecent.html

> I understand that quantifying over functions is formally an “encoding” of operators in ZF, but is there an actual

> difference between the expressivity of TLA+ and second (and higher) -order logic?

TLAPLUS uses a formal system called temporal logic of actions (TLA). It is built over a modal logic called

linear temporal logic (ltl). Inside TLA there is a subset of ZFC (not everything expressible in ZFC

will be supported by TLA).

https://en.wikipedia.org/wiki/TLA%2B

 

And to tell the truth I claim that second-order logic doesn't exist. All the references to it are merely allusive and

contradictory.  It's just like for the Yeti. If you are looking for something of higher order that really exists,

with axioms and all what is needed, try higher-order logic.

 

http://www.sciencedirect.com/science/article/pii/S157086830700081X

 

--

FL

[Stephan Merz]

Ron,

the logic of TLA+ is a first-order logic because you cannot quantify over operators, as in

  \E Op : \A x : Op(x) # x

(However, note that operator definitions in TLA+ can have operator arguments.)

The fact that in set theory, sets (and functions) are ordinary values and so one may quantify over them is confusing at first. As you say, the language "feels" second-order. Formally, it is not because the interpretation of "\in" is only fixed up to the (Zermelo-Fraenkel) axioms.

You may want to look at http://math.stackexchange.com/questions/23799/first-order-logic-vs-second-order-logic and similar references for more in-depth discussions of this.

Concerning your concrete example,

  \E epsilon : \A x : x # {} => epsilon[x] \in x

cannot be proved because the function would have to be "too big" to be a set (its domain would have to contain all values, which is not a set but a class). However, it is easy to prove

  \A S : S # {} => \E epsilon \in [SUBSET S -> S] : \A x \in SUBSET S : x # {} => epsilon[x] \in x

by defining the witness

  eps == [T \in SUBSET S |-> IF T = {} THEN CHOOSE x \in S : TRUE

                                       ELSE CHOOSE x \in T : TRUE]

(The "THEN" branch is necessary to ensure eps \in [SUBSET S -> S].)

Regards,

Stephan

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
Visit this group at http://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.

[Ron Pressler]

Thank you both Stephan and FL. That Math Exchange link was particularly useful. 

So basically, I need to think whether the quantified "operator" (encoded as a ZF function) has a domain that's too big to be a set (I've read the definition in Specifying Systems).  In practice, however, it seems like this can always be avoided, and rather trivially. I have heard people dismiss TLA+ as "not even higher-order (like Coq)", and so less expressive. Similarly, I've heard people say that things like separation logic require higher-orderness, but from what little I've seen of it (which is very little), it also seems to be rather trivially expressed in TLA+. Is there an actual difference in expressiveness or just a formal one?

Ron

[fl]

 

So basically, I need to think whether the quantified "operator" (encoded as a ZF function) has a domain that's too big to be a set

 

I think you need to think that TLA+ only implements a part of ZFC and doesn't allow you to quantify over

variables that you will use to "operate" over something.

 

When you are in doubt with a formal system, look at the formal definition of its syntax and at its system

of axioms and inference rules.

 

--

FL

[fl]

 

When you are in doubt with a formal system, look at the formal definition of its syntax and at its system

of axioms and inference rules.

 

 

Looking at the concept of operators just reminds me that "operators" and functions are

two different things. Look at the syntax. In fact you can quantify over a variable that denotes

a function. It's over an operator that you can't quantify.

 

--

FL

[Ron Pressler]

On Friday, December 4, 2015 at 6:20:50 PM UTC+2, fl wrote:

Looking at the concept of operators just reminds me that "operators" and functions are

two different things. Look at the syntax. In fact you can quantify over a variable that denotes

a function. It's over an operator that you can't quantify.

Oh, I know that. My original question was whether there's a difference (other than in syntax or implementation), and the answer is that there is -- the size of the domain. Now my question is whether the requirement to limit the domain ever makes a difference in practice so that it actually reduces expressivity.

Ron

[fl]

 

> Now my question is whether the requirement to limit the domain ever makes a difference in practice so that it actually

> reduces expressivity.

Use TLAPLUS it is a good system. All what you need to work about an algorithm is here.

 

--

FL

[Stephan Merz]

Each of set theory, higher-order logic (in the tradition of Church's Simple Type Theory, implemented in HOL or Isabelle), and strong type theories as Coq's calculus of inductive constructions has a very different "look and feel". 

Looking at just expressiveness (as in flexibility), set theory is certainly stronger than HOL and I believe also than Coq. For example, HOL or Coq do not admit a set like {1, {2,3}}. In fact, the original motivations for type theory were to tame the expressiveness of set theory because it led to paradoxes.

Whether you need that power in practice is a different question. I have rarely felt bothered by the discipline that HOL imposes, and it helps proof automation. At any rate, TLA+ is more expressive than what you might ever need for specifying algorithms.

Stephan

[Leslie Lamport]

Here is my view, based on almost complete ignorance of the
mathematical foundations and a lot of practical experience using math.
I'm told that second-order logic is more powerful--for one reason,
because it can distinguish between standard and non-standard models of
the integers and first-order logic can't.  I have never found this to
be a practical issue--even in pure math.  I'm certainly not worried
about a bug occurring because an engineer implemented a non-standard
model of the integers.

I don't know Coq, but I'm sure that it's expressive enough
for all practical purposes.  There's no good reason to write a set
like {1, {2,3}}, and making it impossible to write seems like a good
idea.  However, I've found that there is no simple way to make it
impossible to write that set without also making it impossible to
write useful sets.  As this implies, Coq is not simple.  Chris
Newcombe will tell you that one can't expect an engineer to deal with
its complexity.  That doesn't meant that there's anything wrong with
Coq; it just means that it's not meant for ordinary engineers.  For
example, if you look at a math text, you might find that the symbol
+ is used in a single paragraph to mean several different things.
To formalize that math in TLA+, you'd have to use a different symbol
for each of those different meanings.  That would drive a
mathematician crazy.  Coq allows you to use the same symbol for all of
them.  So, as George Gonthier will tell you, you need something like
Coq for formalizing serious math.  Since system builders and algorithm
designers don't use that kind of math, they don't need to deal with
the complexity of a language like Coq.

Leslie

[Chris Newcombe]

  >>As this implies, Coq is not simple.  Chris Newcombe will tell you 

  >>that one can't expect an engineer to deal with its complexity.  

In the paper "Why Amazon Chose TLA+" [0], I wrote:

  "Engineers already have their hands full with the complexity of the problem they 

  are trying to solve. To help them rather than hinder, a new engineering method 

  must be relatively easy to learn and easy to apply. 

... 

  "Methods such as Coq and PVS involve very complicated type-systems and proof

languages. We found these concepts to be difficult to learn. 

...

  "We found that Coq, PVS, and other tools based solely on interactive proof

assistants, are too complicated to be practical for our combination of problem

domain and time constraints."

In that paper I also wrote:

   "We did not find any relevant examples of Coq being used in industry."

Since that paper was written, Coq has been used to prove a safety property (linearizability) of the Raft algorithm for replicated state machines [6], which is (a simplified version of) an algorithm that is used in industry.  This proof was not done directly in Coq; it was done in a language and tool built on top of Coq, called Verdi [1].  Verdi is described "as a framework for implementing and formally verifying distributed systems in Coq" [2].  

Verdi is designed for message-passing algorithms. From the few small examples I've looked at [2], Verdi does appear to be less complex than using Coq directly for that class of problem, at least for the specification part. The main improvement (in my opinion) over plain Coq is that Verdi's conceptual model for specification is quite similar to that of TLA+. In Verdi, a system is specified "by describing the possible “steps” that a system can take during execution.  ...  The possible steps are defined formally as a relation on “worlds”. A world is a snapshot of a system’s execution, and consists of the local state of every node of the system, the set of packets that are in flight, and the trace of external events." [5].

Some other parts of the overall Verdi method are also similar to the TLA+ method.  For instance, proofs of safety properties in Verdi require finding an "inductive state invariant" ([2], section 2.3] 

However, Verdi differs significantly from TLA+ in several ways:

  a. Verdi doesn't yet support specification of fairness, or verification of liveness properties.

  b. Safety is specified as a predicate on traces (behaviors), not a state invariant.

       Example from [2] section 2.1:

"This mutual exclusion property can be expressed as a predicate over traces:

  mutex(t) :=    t = t1 ++ <n1, Grant> ++ t2 ++ <n2, Grant> ++ t3  =>  <n1, Unlock> \in t2

To hold on trace t, the mutex predicate requires that whenever Grant

is output on node n1 and then later Grant is output on node n2, there

must first be an intervening Unlock input from n1 releasing the lock."

   c. Verdi doesn't have a model checker, so all verification is done via proofs in Coq.  In my experience, this will make Verdi impractical for all but the most safety-critical algorithms in industry, unless there has been a major breakthrough reduction in the amount of work and complexity involved in writing proofs.  As far as I can tell, there hasn't been a breakthrough yet; see next two points (d, e).  However, Verdi does include a possibly significant improvement in "automatic refinement" that (the authors claim) reduces the work required to specify and prove systems in less reliable environments, and which therefore might help with industrial systems; see point (f) below.

   d. The proof methods are somewhat different.  From section 2.3 of the Verdi paper[2]:

"The proof that mutex holds on all traces of the lock service application consists of three high-level steps: 

   (1) prove an invariant about the reachable node and network states of the lock service application, 

   (2) relate these reachable states to the producible traces, and 

   (3) show that the previous two steps imply mutex holds on all producible traces"

      The paper goes on to describe how part #1 requires finding a state predicate (called mutex_state in the paper), which to me appears to be a conventional safety property, i.e. an invariant of reachable states.  To prove that invariant, the method requires finding an "inductive state invariant".  So part #1 appears to match the main idea of safety proofs in TLA+. But part #2 and #3 are different - at least superficially - to how things are done in TLA+. See the paper for description and example of part #2 and #3 (for brevity I won't quote those sections here).

      I'm not qualified to comment on whether the proof method in Verdi is novel, or whether the differences with the TLA+ proof method are an improvement or a re-casting. As Verdi is based on Coq, I assume that Verdi is sound and relatively complete.  

      I have doubts about how practical the Verdi method is for complex systems (i.e. systems more complex than basic Raft), because Verdi's use of traces (behaviors) to specify correctness properties, to model state ('worlds' always include traces of past events and messages), and in proofs (parts 2 and 3 of the method) appear to introduce a dimension of behavioral reasoning.  Caveat: this is merely a suspicion on my part, not based on any solid evidence.  But if it is the case then, I also suspect that the method would have the problem of combinatorial explosion of cases, due to the many possible permutations and interleavings of events allowed by any real-world specification.  Perhaps Verdi solves that problem, but I did not find it mentioned in the paper [2].

      For this reason, I still prefer the more direct TLA+ method of proof solely by inductive invariance (occasionally using an explicit history variable if necessary).  However, my preference doesn't actually get me anywhere, as I've never successfully proven the correctness of a real industrial system in TLAPS. The main reason I've failed is that it's too difficult and time-consuming for me, and for all software engineers in industry that I've discussed this with, to find the inductive invariant for a real-world system. That central problem appears to be common to both TLA+ and Verdi.

      I don't know whether Verdi/Coq has useful tools to help incrementally find ('debug') an inductive invariant.  This is an area in which TLA+ does need better tools. In TLA+ the standard method is to ask TLC to model-check  Inv /\ Next => Inv'  but TLC usually can't do that for a complex spec, e.g. from industry.  The next best option that I'm aware of is to use the TLA+-to-ProB translator and the ProB constraint solver, but I haven't tried that approach on an industry spec. (Last time I checked, the ProB translator supported a large subset of TLA+ but not the whole language, which is entirely understandable as ProB is typed and TLA+ is not.)  The next best option is to manually convert the spec to Alloy (as the Alloy Analyzer can check inductive invariance), but Alloy is far less expressive than TLA+.  The best option for the future might be the unfinished symbolic model checker for TLA+ that was never released. But someone would have to finish it; a huge project.

  e. Even after an inductive invariant is found, proofs in Verdi still appear to require a lot of expertise with the Coq proof system and manual effort.  I may be wrong about this, as I haven't tried it myself.  My current view is based on the following information:

    i. Proofs in Verdi are fairly large; I'd estimate at least as large as TLAPS proofs of the same system (when using the SMT backend).  

       E.g. [2] reports:

         - 500 lines to prove safety (mutual exclusion) for the 40-line spec of the (very) simple lock server specified in [2].

         - 4144 lines to prove safety (linearizability) of the 170-line spec of basic Raft algorithm for replicated state machine. (I call this the 'basic' algorithm as the spec did not include important and infamously non-trivial features required in industry, such as log compaction and dynamic group membership.)

    ii. Seven people worked on the proof of basic Raft.  The people were the designers of Verdi, so presumably had significant prior experience using Coq.  I can't find any description of how long the proof took in person-hours.

    iii. To me (a non-user of Coq) the proof language still looks extremely complicated.  See the many files in [5].  The proof is much harder to understand than a TLAPS proof (after reading the appropriate short section of the hyperbook on the TLAPS proof language).  Some reasons:

            - The Verdi proof lacks the hierarchical structure that TLAPS uses to manage complexity.  Instead it uses many lemmas, which I find harder to follow.

            - The Verdi proof justifications are invocations of Coq heuristics that are very hard to understand.

         The total lack of explanatory comments doesn't help.

  f.  Verdi has support for a limited form of 'automated refinement' that TLA+ does not have.  I find this to be the most interesting part of Verdi. From [2]:

"Verdi eases the verification burden by enabling the developer to first verify their system under an idealized fault model, then transfer the resulting correctness guarantees to a more realistic fault model without any additional proof burden"

      From the paper, the current automated refinements include i) adding sequence numbers to network messages to eliminate concerns about message loss, duplication and reordering, and ii) using replicated state machines to implement fault tolerant processes. These are a good start, but in real industrial systems such mechanisms often have to co-operate in order to implement a higher-level correctness property (e.g. transaction isolation in a database), so it remains to be seen how far this idea will go in practice. If it becomes sufficiently flexible then it could be very valuable.

  g. Verdi generates executable code in OCAML, which according to results in [2] appears to be fairly efficient for simple benchmarks.  This is obviously a benefit.  However, in order to be used in a real industrial system the code will need to be modified in many ways (security, operational visibility and control, support online deployment & rollback of changes to the code, multi-core scalability etc. etc), so the question arises of re-verification in the presence of constant maintenance.  Still, it's a very welcome direction.

So Verdi is an interesting approach for message passing algorithms, and is particularly impressive because of (f) and (g) above.  But I believe that TLA+ is a significantly better method for use in industry, because TLA+ addresses a much larger class of problems (in addition to message-passing algorithms I've used TLA+ for shared-state concurrent algorithms, sequential algorithms, conceptual modeling & data modeling), and because of the other factors mentioned above and in [0].

regards,

Chris

[0] "Why Amazon Chose TLA+"  http://research.microsoft.com/en-us/um/people/lamport/tla/amazon.html

[1] Verdi's website: http://verdi.uwplse.org/   

[2] The Verdi paper:  http://verdi.uwplse.org/verdi.pdf

[3] An introduction to Verdi by one of its designers: http://homes.cs.washington.edu/~jrw12/network-semantics.html

[4] A comment from a designer of Verdi:  https://news.ycombinator.com/item?id=10017549

[5] https://github.com/uwplse/verdi/tree/master/raft-proofs 

    and https://github.com/uwplse/verdi/tree/master/raft 

[6] https://raft.github.io/

[Ron Pressler]

Thank you for the detailed response! 

There is no doubt that any proof system is probably too expensive for use in the industry, both because of the correctness requirements that are somewhat relaxed and because the systems tend to be more complicated than idealized algorithms. I was just interested in the more theoretical mathematical implications of the dependent-type vs set-theory approaches, just out of intellectual curiosity (now that I've started using TLA+, I'm interested in other approaches).

In any case, going on a tangent, I was surprised to read your mention of an incomplete symbolic model checker. After growing to enjoy TLA+ so much, that was the first thing that I thought would be a great addition, as it would allow checking of different kinds of specs, like sorting algorithms (a very interesting bug -- which only occurs on very large arrays -- was found in Java's sorting algorithm using the KeY project for symbolic execution) and order-dependent data structures like B-trees, where small models are ineffective. Any more information on this effort? It's the first time I hear of it. I would imagine that given TLA+'s simple and clear semantics, implementing symbolic execution would be easier than for something like Java.

Ron

[Leslie Lamport]

I'm not sure what symbolic execution encompasses.  Complexity isn't the issue; it's expressiveness.  Complexity of an inexpressive language can be overcome with a lot of fairly easy work.  The partially developed symbolic model checker is BDD based.  BDD model checking essentially require static typing of the spec, which is in general impossible and which seems to be impossible in practice for a suitably general class of TLA+ specs.  However, a BDD model checker is possible because you don't have to statically type the spec--you just have to type a finite model of the spec.  That turns out to be possible in practice.  A BDD model checker for a fragment of TLA+ was built in one summer by an intern.  My understanding is that all the hard problems have been solved, and it just requires extending it to handle the full language.  But hard problems are usually hard to anticipate.

Leslie

[Michael Leuschel]

Hi Ron,

Do you have a TLA+ spec of the flawed sorting algorithm ?

On 6 Dec 2015, at 18:39, Ron Pressler <r...@paralleluniverse.co> wrote:

 (a very interesting bug -- which only occurs on very large arrays -- was found in Java's sorting algorithm using the KeY project for symbolic execution) 

I am also not sure what kind of symbolic execution you are after.

The answer of Leslie Lamport refers to BDD-based symbolic model checking.

The ProB tool can be used for constraint-based symbolic execution, which in turn can be used for bounded model checking or test-case generation.

Below is an artificial example, where the ProB bounded model checker finds a counter-example (Init with ct=33554431 followed by Inc(1)) immediately by solving the corresponding constraints, but the explicit model checking with TLC reports: "Too many possible next states…"

Is this the kind of symbolic execution you are after ?

Of course, ProB’s support for TLA+ is unfortunately still limited (the TLA+ specs have to go through a typechecker, no support for user-defined recursive operators,… ); but we would be happy to try out more involved examples.

Greetings,

Michael

---- MODULE VerySimpleCounterWrongLargeBranching ----

EXTENDS Integers

VARIABLES ct

lim == 2^25

Invariant1 == ct \in Int

Invariant2 == ct < lim

Init == ct \in (0 .. lim - 1)

Inc(i) == ct + i =< lim

/\ ct' = ct + i

Reset == ct = lim

/\ ct' = 0

Next == \/ \E i \in (1 .. 1000) : Inc(i)

\/ Reset

==== 

The config file is:

INIT Init

NEXT Next

INVARIANT Invariant1

INVARIANT Invariant2

[Ron Pressler]

On Sunday, December 6, 2015 at 11:43:02 PM UTC+2, leuschel wrote:

Do you have a TLA+ spec of the flawed sorting algorithm ?

No, but the algorithm, as well as a formal specification of the broken assumed invariants and an account of the bug and its discovery, can all be found here. 

 

I am also not sure what kind of symbolic execution you are after.

The answer of Leslie Lamport refers to BDD-based symbolic model checking.

I am not too sure either (as I am not well-versed in the taxonomy of formal methods), but the kind of symbolic execution used in KeY :) I believe it is not the same as BDD model-checking.

A tool that is able to automatically check sorting algorithms is a very powerful one to have in your toolbelt, as sorting algorithms -- like state machines -- are exemplars of a very large class of algorithms and data structures (heaps, B-trees and many other kinds of trees, other indexes in general), and if you can check them, you can probably check many interesting programs.

Ron

[Stephan Merz]

Let's just try to be clear about terminology: KeY is an interactive theorem prover that includes an expansion strategy based on symbolic execution (typically, for unfolding a recursive call of a method). The user experience of writing proofs in KeY is closer to writing a TLA+ proof using TLAPS than calling a model checker or constraint solver, which are fully automatic. In particular, KeY requires inductive invariants, and can prove correctness for arbitrary instances.

Regards,

Stephan

[Ron Pressler]

On Monday, December 7, 2015 at 2:19:25 PM UTC+2, Stephan Merz wrote:

Let's just try to be clear about terminology: KeY is an interactive theorem prover that includes an expansion strategy based on symbolic execution (typically, for unfolding a recursive call of a method). The user experience of writing proofs in KeY is closer to writing a TLA+ proof using TLAPS than calling a model checker or constraint solver, which are fully automatic. In particular, KeY requires inductive invariants, and can prove correctness for arbitrary instances.

You are absolutely right. I was under the false impression that KeY is an automatic tool.

Ron

[Michael Leuschel]

Hi Ron,

we have had a look at the link about the sorting algorithm flaw you posted. It also mentions the binary search algorithm overflow flaw.

We have done a few models of the flawed binary search algorithm and our bounded model checker can be used to find overflows.

Below is the PlusCal/TLA+ version that Dominik wrote.

The (very short) counter example is shown in the PDF below.

We are currently working on improving the bounded model checking of ProB (experimenting with various algorithms) and also try to improve the support for TLA+.

If you or anybody else has interesting, challenging TLA specs, we are happy to try and have a look at them.

Note: the larger you make mxint, the longer it takes to find the counter-example, as the constraint solver also has to construct a very large, sorted array as input.

I would be interested in also trying out the timSort Algorithm mentioned in the link you posted;  here at least the required counter examples should be smaller than for binary search, but the algorithm is much more involved.

On 7 Dec 2015, at 11:23, Ron Pressler <r...@paralleluniverse.co> wrote:

Do you have a TLA+ spec of the flawed sorting algorithm ?

No, but the algorithm, as well as a formal specification of the broken assumed invariants and an account of the bug and its discovery, can all be found here. 

Greetings,

Michael

---------------------------- MODULE BinarySearch ----------------------------

EXTENDS Integers, TLC, Sequences

mxint == 127

myNAT == 0..mxint

myINT == (-mxint)..mxint

CONSTANTS arr, goal

arr1 == <<-1,0,1,2,3,5>>

goal1 == 2

sze == Len(arr)

ASSUME sze \in myNAT

(* ASSUME sze <mxint *)

PartialFunctions(S, T) ==  UNION{[x -> T] :x \in SUBSET S}

Range(f) == {f[x] : x \in DOMAIN f}

isEleOfParFunc(f, S, T) == DOMAIN f \subseteq S /\ Range(f) \subseteq T 

ASSUME 

  /\ isEleOfParFunc(arr, myNAT, myINT)

  /\ arr \in [1..sze -> myINT]

  /\  \A i \in 1 ..(sze - 1) : arr[i] =< arr[(i + 1)]

ASSUME goal \in myINT

(*

--algorithm contraints

variable found = FALSE; i = 1; j = sze; mid = 0;

begin

    while found = FALSE /\ i <= j

    do

        mid := i+j;

        mid := mid \div 2;

        if arr[mid] = goal

        then 

          found:= TRUE; 

          i := mid; 

          j := mid; 

        elsif arr[mid] < goal then i := mid + 1;

        else j := mid - 1;

        end if;

    end while;

end algorithm

*)

\* BEGIN TRANSLATION

VARIABLES found, i, j, mid, pc

vars == << found, i, j, mid, pc >>

Init == (* Global variables *)

        /\ found = FALSE

        /\ i = 1

        /\ j = sze

        /\ mid = 0

        /\ pc = "Lbl_1"

Lbl_1 == /\ pc = "Lbl_1"

         /\ IF found = FALSE /\ i <= j

               THEN /\ mid' = i+j

                    /\ pc' = "Lbl_2"

               ELSE /\ Assert(1=1, 

                              "Failure of assertion at line 46, column 5.")

                    /\ pc' = "Done"

                    /\ mid' = mid

         /\ UNCHANGED << found, i, j >>

Lbl_2 == /\ pc = "Lbl_2"

         /\ mid' = (mid \div 2)

         /\ IF arr[mid'] = goal

               THEN /\ found' = TRUE

                    /\ i' = mid'

                    /\ j' = mid'

               ELSE /\ IF arr[mid'] < goal

                          THEN /\ i' = mid' + 1

                               /\ j' = j

                          ELSE /\ j' = mid' - 1

                               /\ i' = i

                    /\ found' = found

         /\ pc' = "Lbl_1"

Next == Lbl_1 \/ Lbl_2

           \/ (* Disjunct to prevent deadlock on termination *)

              (pc = "Done" /\ UNCHANGED vars)

Spec == Init /\ [][Next]_vars

Termination == <>(pc = "Done")

\* END TRANSLATION

Inv == 

 /\ found \in BOOLEAN 

 /\ i \in myNAT

 /\ j \in myNAT

 /\ mid \in myNAT

=============================================================================

\* Modification History

\* Last modified Wed Dec 09 14:53:25 CET 2015 by hansen

\* Created Wed Dec 09 10:14:15 CET 2015 by hansen

[Ron Pressler]

Nice! This means that we can also use TLA+ to spec and check all sorts of order-based algorithms.

If you're interested in algorithms to check, I would suggest a B-tree (here's a short implementation).

Ron