3 ms·

So this system uses the spec language ACSL (I assume it's a formal spec language, FSL). How widely used is it? I've heard of TLA+ being very popular. Then ther

So this system uses the spec language ACSL (I assume it's a formal spec language, FSL). How widely used is it? I've heard of TLA+ being very popular. Then there is Z notation, and about half a dozen or more others. If there is no standard FSL, do I have to learn a new FSL everytime I want to apply formal methods to a slightly different system I'm working with? Formal methods is a hard enough area. Lack of standardization makes it harder.

Firobe 6y ago
ACSL is indeed a FSL. Making a standard FSL is a nigh impossible since it should encompass every programming language and its specific features. For example, ACSL has built-in ways to talk about the side effects in C, labels, the validity of pointers, etc. and the semantic of those elements is tied to the C standard. On the other hand, the syntax of ACSL is heavily inspired from JML (FSL for Java) which is pretty popular. So if you know JML, it's easy to learn ACSL (you just have to learn C-specific features)