#formal-verification Activity Feed

I spent some time improving Saffron, a formal language I've been working on aimed at requirements elicitation and analysis.

Mainly I've been thinking about how to express common "patterns" in the underlying formalism e.g. "A message has a single author" can be expressed as infer WHERE m:Message a:Actor b:Author MATCH Author(m,a) THEN PROHIBIT Author(m,b).

One of my goals for this week is to document some of these patterns, and perhaps allow them to be expressed in a syntactic sugar e.g. the above is perhaps more nicely expressed as constrain WHERE m:Message a:Actor EXCLUSIVE Author(m,a)

(An even better syntactic sugar might be to allow the construction of meta-types that compile down to such relationships under the hood to allow a more programmer friendly representation e.g. struct Message := { Author Content } though I am less inclined towards that direction right now as it clutters the number of formalisms at the highest level.)


Posted: by Sarah Jamie Lewis


Home ยป Activity Feed