Comment by ok123456
3 days ago
In wider practice, UML (class diagrams) is never used by working software developers as a frontend to formal methods.
It got pushed on everyone, so there could be a layer of "software architects" who didn't have to know how to code and could have endless meetings where the final product was a Bayeux Tapestry of UML.
UML captures inheritance and composition well, but a program is more than the sum of its schema. Also, real programming languages all have their idioms, and using UML as the design space creates a significant impedance mismatch.
It is the complete modeling language (class diagram is just one artifact) that people are looking at using with Formal Methods along with regular Software Engineering. For example Sequence Diagrams are extremely useful in understanding the dynamic nature of a System. Lots of papers have been published, IEEE workshops and there is even an attempt at integrating the B Method with UML to give a UML-B variant. Like any language it is up to the developer to study it and learn to use it productively in his work. Of course it is not the "in thing" but quite useful nonetheless when used appropriately.
Automatic Formal Model Generation from UML Diagrams – An Implementation Experience - https://ieeexplore.ieee.org/document/9753518
UML-B: Formal modelling and design aided by UML - pdf at https://citeseerx.ist.psu.edu/document?repid=rep1&type=pdf&d...