[tlaplus] TLA+ and C++ templates

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

I have been thinking about ways to verify C++ templates, and I wonder if TLA+ would be good for this?

I can quite trivially (for example) write a PlusCal spec to verify std::find for a specific input type, but is there a way to explore the state space for all types of data that might be in the array? 

I have the below, which does not initialise the array to be anything, but that seems to default set it to zero.

-------------------------------- MODULE find  -------------------

EXTENDS Naturals, TLC, Integers

CONSTANT n

(* --algorithm find 

variables first = 1, last \in 1 ..  n , value, array = [k \in 1 .. n |-> 0],

begin    

assert last >= first;

    while first /= last do

        if array[first] = value then

            skip;

        end if;

       first := first + 1; 

     end while;    

end algorithm *)

-- 
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/c76a27c0-2188-4620-8e77-f4b9de8904b5n%40googlegroups.com.