[tlaplus] Modeling an object oriented design

[Imran Meah <imranmeah91@xxxxxxxxx>]

There used by a modeling language called 

LePUS3 (https://en.wikipedia.org/wiki/LePUS3) which was used to formally model object oriented design.  It was popular in 2000s  but seems to have disappeared about 10 years ago.

With that I am exploring using TLA+ for formally modeling an object oriented design. 

The way I see it should be workable solution.

Class/Object are represented as data structure , I think we call them record in TLA+.

Define transition rules that will mutate this object. 

So far, I am still pondering how to model a class instantiation as in creation of an object from class. I guess if it is singleton pattern, it wouldn't matter. 

My goals:

to start with      -Use TLA+ as tool to understand complex object oriented design

Next step-Try modeling checking some invariants.

Would be nice- To visualize the model in some form of diagram. 

What I am looking for:

Is TLA+ suitable for object oriented modeling/specification. Is there precedent for this application?  

-- 
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/32d0d40d-11d8-4fe7-942d-75613e4358fen%40googlegroups.com.