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

*From*: "christin...@xxxxxxxxx" <christina.a.burge@xxxxxxxxx>*Date*: Mon, 10 Jul 2023 05:10:21 -0700 (PDT)

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.

**Follow-Ups**:**Re: [tlaplus] TLA+ and C++ templates***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus]** - Next by Date:
**Re: [tlaplus] TLA+ and C++ templates** - Previous by thread:
**Re: [tlaplus] after installation of tlaps, "Prove Step or Module" fails with Java NullPointerException** - Next by thread:
**Re: [tlaplus] TLA+ and C++ templates** - Index(es):