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

*From*: "christin...@xxxxxxxxx" <christina.a.burge@xxxxxxxxx>*Date*: Fri, 28 Jul 2023 07:15:14 -0700 (PDT)*References*: <98c9141f-b327-4575-b4d1-d50471c1bc73n@googlegroups.com> <c932fff2-f0db-5a2f-a659-2940dea87097@gmail.com>

I want to thank you so much for that comprehensive explanation! I have already skimmed it, and I am going sit down and read it properly, thank you again!

On Wednesday, July 26, 2023 at 11:59:20 AM UTC+1 Martin wrote:

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+u...@xxxxxxxxxxxxxxxx

> <mailto:tlaplus+u...@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/51d6d86e-8353-47a0-a43b-ab990d168690n%40googlegroups.com.

**Follow-Ups**:**Re: [tlaplus] Verifying c++ templates***From:*christin...@xxxxxxxxx

**References**:**[tlaplus] Verifying c++ templates***From:*christin...@xxxxxxxxx

**Re: [tlaplus] Verifying c++ templates***From:*'Martin' via tlaplus

- Prev by Date:
**Re: [tlaplus] Verifying c++ templates** - Next by Date:
**[tlaplus] Re: Checking data type Pluscal** - Previous by thread:
**Re: [tlaplus] Verifying c++ templates** - Next by thread:
**Re: [tlaplus] Verifying c++ templates** - Index(es):