I'm curious if a generally recursive algorithm can be treated in TLA+ without finitizing the model. For instance, for any given tree, we could prove properties of a BFS procedure on it, but can we do so for all trees?
I was curious if anyone knew of existing formal specifications (in TLA+ or any other form) of various graph search algorithms e.g. breadth first search, depth first search. I was looking around at various definitions of depth first search in textbooks (e.g. CLRS), etc. but didn't seem to find a place where a precise, high level specification of the algorithm is given.
--
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/9abc0cdb-1277-4987-b163-def0a2a64cc8n%40googlegroups.com.