[tlaplus] Re: Modeling an object oriented design

[recepient recepient <netsmaza@xxxxxxxxx>]

Long time programmer here learning TLA+ ... I agree with Alex's assessment: TLA+ is not best used to model UML or static class diagrams. In fact unless I was working on cache coherence or a router algorithm fairly single threaded --- extremely combinatorial and difficult algos --- or distributed systems on the other extreme, I'd prefer to rely on Hoare logic, Frama-C, unit & integration testing. TLA+ is good for when (*) you have communication sequential  systems has you have no idea if your exactly-once-message-processing strategy works or, whoops, it hadn't occurred to one that was a real issue. See https://github.com/rodgarrison/tla_note1 "A Note on Formal Specification for Programmers."

On Wednesday, December 2, 2020 at 4:12:51 PM UTC-5 imran...@xxxxxxxxx wrote:

Alex, 

Thanks, I wasn't aware TLA+ has visualization functionality. I will check it out.

On Wednesday, December 2, 2020 at 8:02:57 AM UTC-6 alex.we...@xxxxxxx wrote:

TLA+ encourages algorithmic thinking which is independent of any programing language or paradigm. So I would focus on:

- what are the state variables of your algorithm. These get encoded in TLA+ via VARIABLES

- what are the allowed transitions between states. These are the actions, i.e. v' = <new value>

These concepts are all you need to model an algorithm.

Re visualization: When you create a model for your spec, there is an option to export the discovered state space as a graphviz state diagram. I use this all the time to get an understanding of the state space of the algorithm. Of course, be careful, because some state spaces can be very large. In that case, the program will be unable to export the diagram, or if it can it will be unreadable.

 

In this case, try and create a model which is bounded by some configurable CONSTANTS which you can create more or less of in your model.

On Tuesday, December 1, 2020 at 11:43:12 PM UTC-5 imran...@xxxxxxxxx wrote:

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/9b6f0217-9ff6-4b76-9414-2813b66b7ba3n%40googlegroups.com.