Re: [tlaplus] TLA+ logic

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...@xxxxxxxxxxxxxxxxxxx> 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