[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] Verifying c++ templates
Hello!
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)!
cheers,
Martin
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
CONSTANT Values, K
(*
--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")
\* END TRANSLATION
FindsElement == (index > 0) => (elements[index] = what)
ErrorMeansNotContained == (index <= 0) => (\A i \in 1 .. Len(elements) : elements[i] # what)
Correct == pc = "Done" => (FindsElement /\ ErrorMeansNotContained)
=============================================================================