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

[tlaplus] Verifying c++ templates

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.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/98c9141f-b327-4575-b4d1-d50471c1bc73n%40googlegroups.com.