[tlaplus] Verifying c++ templates

["christin...@xxxxxxxxx" <christina.a.burge@xxxxxxxxx>]

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.