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

[tlaplus] Re: Using TLA+ for data modeling



Chris,

Looking back at this I wish it had not taken me so long to understand it. Having now played with TLA+, I think everything you've said is spot-on.

However I think that for designing and implementing real systems, a more humanised approach than TLA+ is needed to defining operations. I've written to you privately about the "decision/action" extensions to CQL, which I think others here might wish to enquire about. I won't dump my thoughts into this old thread, but just mention that I'm still thinking about this problem. Rather than merely verifying the code, the specification could be generated to a guaranteed-correct implementation. With the operations defined in the syntax of the model, any error scenarios that TLA+ finds could also be verbalised. In other words, it could explain in English why your code is wrong and how it will fail. 

Also, the CQL specification has been rewritten and is published at <http://cjheath.github.com/activefacts-cql> in case anyone is wanting that.

Further, on verbalisation, I have now received a copy of the PhD thesis by Shin Huey where she developed ORMv2 verbalisations for Mandarin and Malay. It was a more difficult problem even than Terry Halpin expected, but it is done!

Clifford Heath.

--
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/f944a6db-7453-4417-bd6c-44651d05e549%40googlegroups.com.