[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

# 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 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, Sequencesmxint == 127myNAT == 0..mxintmyINT == (-mxint)..mxintCONSTANTS arr, goalarr1 == <<-1,0,1,2,3,5>>goal1 == 2sze == Len(arr)ASSUME sze \in myNAT(* ASSUME sze 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 contraintsvariable 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 TRANSLATIONVARIABLES found, i, j, mid, pcvars == << 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]_varsTermination == <>(pc = "Done")\* END TRANSLATIONInv ==  /\ 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

Attachment: BinarySearch_counter.pdf
Description: Adobe PDF document