Formal Specification Using ErgoAI or Flora-2

[Rangarajan Krishnamoorthy]

Hi,

I am interested in the area of Formal Specification and one of the topics I am considering for writing a blog on is to show how we can use Flora-2/ErgoAI to model a formal specification similar to Z or VDM. I got started on this and even spent a few hours, but couldn't get far. The main emphasis in Z and VDM is to be able to precisely specify the various types and their constraints corresponding to the domain being modelled. I am having trouble doing this in Flora-2 (did not look at Ergo in this context). Another related issue is that Section 43.2 of Flora User Manual says that type checking is currently not done. This means, even if I am able to syntactically capture a formal spec, it cannot be validated. I feel it would be very useful if Flora-2/Ergo could be gainfully applied in this problem domain.

Please comment.

Regards,

Rangarajan

[michae...@coherentknowledge.com]

You can check the type constraints (and other constraints) by posing them as queries.  Flora-2 provides canned queries for that.  Ergo, in addition, supports constraints and alarms as builtin features, which can make constraint checking automatic.

Michael Kifer

[Rangarajan Krishnamoorthy]

That sounds interesting. Will give it a try.

Thanks,

Rangarajan

-- 
You received this message because you are subscribed to the Google Groups "ErgoAI, Flora-2, and XSB Users Forum" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ErgoAI-Flora2-XSB...@coherentknowledge.com.
To post to this group, send email to ErgoAI-Flor...@coherentknowledge.com.
Visit this group at https://groups.google.com/a/coherentknowledge.com/group/ErgoAI-Flora2-XSB-forum/.
To view this discussion on the web visit https://groups.google.com/a/coherentknowledge.com/d/msgid/ErgoAI-Flora2-XSB-forum/4774302d-66fe-471b-925f-ec67a443c107%40coherentknowledge.com.