axiomatic blocks as namepaces

[jensgerlach]

I think an axiomatic block should declare a separate namespace. Instead of

/*@ axiomatic sign {
   @  logic integer get_sign(real x);                                                                                                               
   @  axiom sign_pos: \forall real x; x >= 0. ==> get_sign(x) == 1;                                                                                                                 
   @  axiom sign_neg: \forall real x; x <= 0. ==> get_sign(x) == -1; 
   @}
@*/

one could then omit the sign_ prefix for the individual axioms.

/*@ axiomatic sign {
   @  logic integer get_sign(real x);                                                                                                               
   @  axiom pos: \forall real x; x >= 0. ==> get_sign(x) == 1;                                                                                                                  
   @  axiom neg: \forall real x; x <= 0. ==> get_sign(x) == -1; 
   @}
@*/

[vprevosto]

Sorry, for the delay in answering, but I'd tend to say the need for namespaces is covered by the (unimplemented in Frama-C) module feature described in section 2.6.11

[jensgerlach]

For me, modules group specification elements, as do C++ namespaces group classes, functions and global variables. Still, a single C++ class (or C struct) is a namespace in its own right. Taking this point of view, I continue to wish for axiomatic blocks being a namespace.

[vprevosto]

If I understand well your comment, we could say that an axiomatic block would implicitly give rise to a module of the same name, so that, in your example, we would have the axioms sign::pos and sign::neg (and, supposing we abbreviate get_sign into get sign::get). Of course, 2.6.11 admittedly should introduce the equivalent of C++ using directive in order to use shorter names when appropriate.