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

Re: [tlaplus] Verifying c++ templates


Usually you check your specification against a property (for example that find returns a valid index of the element you are looking for). So if TLC doesn't report an error it foremost means that it could successfully check that the property holds for all runs of the specification you wrote.

There are two things to be aware of though:

* A specification disregards parts of the "real world" (in your case a C++ program?) and you need to decide what level of detail you want to model. For example you already saw that TLA+ is a logic based on mathematics (sets, unbounded integers, sequences) and C++ constructs often don't have direct correspondences in TLA+. This is absolutely fine: if you want to check if an algorithm finds an element you can first ignore the memory layout. Rightly you would object that this doesn't imply that the C++ implementation is correct. But if the algorithm is not correct, the implementation can't be and that's what we use TLA+ for. It is possible to encode more parts of C++ into TLA+ (e.g. pairing a sequence with a number to distinguish different memory positions) but then you will find implementation errors (overflows, etc.), not conceptual errors (and this is where TLA+ shines). In any case there is some gap between model and reality that we need to accept so depending on what kind of bugs we are looking for we need to change our approach.

* TLA+ itself is more expressive than what can be can be model checked by TLC. For example TLC can only check find on a finite number of values. Since sequences can be of any length (i.e. there are infinitely many) you need to focus on a treatable subset (e.g. by investigating sequences only up to a specific length - if an element of the sequences comes from an infinite set, that might need to be bounded too). Interestingly, at least according to folklore, a lot of conecptual mistakes already occur for relatively small sets. See for example the attached Find.tla: to model check it you need to find sensible values for the set of elements (Values) and the maximum length (K) for TLC (e.g. Values = {1,2,3,4} and K = 3). If you run TLC checking the invariant Correct you will find that we have an off by one error in loop condition (due to sequence indices starting at one it must <= Len(elements) ). That's by no means a complete procedure but it works amazingly well. If you want to make sure this runs for all sequences, you can use the TLA Proof System (TLAPS) for this. Please be aware that writing a proof should only come after you have thoroughly model checked your specification and if you really need that level of confidence since writing proofs takes much more time than writing spec.

I hope that helps a bit (and doesn't contain any unmentioned errors)!


On 7/26/23 03:16, christin...@xxxxxxxxx wrote:
You may have seen my other thread about verifying c++ templates. I have a couple of more general questions which almost certainly expose my lack of understanding, but here goes!

If I verify (for example) std::find for every data type that TLA+ supports, am I right in thinking that I have verified the C++ template only for the corresponding types in C++?

TLA+ doesn't have pointers. In the case of templates which make use of pointers, if I write the specification in a way which gets around this, have I really verified that template?

Are there other limitations I'm not thinking of?

Thanks in advance!

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+unsubscribe@xxxxxxxxxxxxxxxx <mailto:tlaplus+unsubscribe@xxxxxxxxxxxxxxxx>. To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/98c9141f-b327-4575-b4d1-d50471c1bc73n%40googlegroups.com <https://groups.google.com/d/msgid/tlaplus/98c9141f-b327-4575-b4d1-d50471c1bc73n%40googlegroups.com?utm_medium=email&utm_source=footer>.

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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/c932fff2-f0db-5a2f-a659-2940dea87097%40gmail.com.
-------------------------------- MODULE Find --------------------------------

EXTENDS Integers, Sequences, SequencesExt



--fair algorithm Find {
  variables index = 0;  current_index = 1, elements \in BoundedSeq(Values, K), what \in Values;

    while (index = 0 /\ current_index < Len(elements)) {
        if (elements[current_index] = what) {
            index := current_index;
        } else {
            current_index := current_index + 1


\* BEGIN TRANSLATION (chksum(pcal) = "7c28162a" /\ chksum(tla) = "92a83823")
VARIABLES index, current_index, elements, what, pc

vars == << index, current_index, elements, what, pc >>

Init == (* Global variables *)
        /\ index = 0
        /\ current_index = 1
        /\ elements \in BoundedSeq(Values, K)
        /\ what \in Values
        /\ pc = "Lbl_1"

Lbl_1 == /\ pc = "Lbl_1"
         /\ IF index = 0 /\ current_index < Len(elements)
               THEN /\ IF elements[current_index] = what
                          THEN /\ index' = current_index
                               /\ UNCHANGED current_index
                          ELSE /\ current_index' = current_index + 1
                               /\ index' = index
                    /\ pc' = "Lbl_1"
               ELSE /\ pc' = "Done"
                    /\ UNCHANGED << index, current_index >>
         /\ UNCHANGED << elements, what >>

(* Allow infinite stuttering to prevent deadlock on termination. *)
Terminating == pc = "Done" /\ UNCHANGED vars

Next == Lbl_1
           \/ Terminating

Spec == /\ Init /\ [][Next]_vars
        /\ WF_vars(Next)

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


FindsElement == (index > 0) => (elements[index] = what)
ErrorMeansNotContained == (index <= 0) => (\A i \in 1 .. Len(elements) : elements[i] # what)

Correct == pc = "Done" => (FindsElement /\ ErrorMeansNotContained)