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

[tlaplus] TLA+ and C++ templates

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


(* --algorithm find 

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


assert last >= first;

    while first /= last do

        if array[first] = value then


        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.