[feature] Model_Of aspect to specify external subprograms

[danielmercier]

Summary

This RFC proposes a new Ada aspect, Model_Of, intended for use by analysis tools to associate additional specification information with an existing subprogram. The aspect allows tools to link a model subprogram, declared separately in a specification package, to an original subprogram, and to treat any aspects applied to the model as if they were applied to the modeled subprogram for analysis purposes.

Suppose an existing package contains a subprogram that cannot be modified:

package Math is
   function Sqrt (X : Float) return Float;
end Math;

An analysis tool may require a more robust specification. A separate specification package can be written:

package Math_Models is
   function Sqrt (X : Float) return Float
     with
       Model_Of => Math.Sqrt,
       Pre  => X >= 0.0,
       Post => Sqrt'Result >= 0.0;
end Math_Models;

Motivation

Analysis tools such as formal verifiers, abstract interpreters, or linters often require additional semantic information that cannot always be directly embedded in production source code. Reasons include:

• The original subprogram belongs to third-party or legacy code.
• The original code must remain free of tool-specific annotations.
• Alternative or abstract specifications are needed for verification or modeling purposes.

Currently, there is no standardized mechanism in Ada to express that one subprogram declaration models another, nor to propagate aspects from a model declaration to the original subprogram in a tool-recognizable way.

The Model_Of aspect addresses this gap by enabling the declaration of a subprogram that mimics an existing one and explicitly links to it. Analysis tools can then use this relationship to augment or replace the original specification without modifying the original source.

Caveats and alternatives

• Introduces a concept that is meaningful only to analysis tools.
• Requires tools to implement additional consistency checks.
• May lead to fragmented specifications if overused.

However, not introducing this feature forces tools to rely on naming conventions, external configuration files, or source rewriting.

[sttaft]

Looks very interesting. It might be worth considering Model_Of at the package level, since typically you are going to create a complete model package with multiple subprograms. Also, many pre/postconditions refer to package state, so the package seems like it might be a more natural unit for this kind of modeling.

[danielmercier]

Looks very interesting. It might be worth considering Model_Of at the package level, since typically you are going to create a complete model package with multiple subprograms. Also, many pre/postconditions refer to package state, so the package seems like it might be a more natural unit for this kind of modeling.

Having Model_Of on the package is certainly interesting, perhaps as an addition rather than a complete replacement. It could also be a neat way to annotate generic packages: you could copy the formal part of the package you want to model, add Model_Of to this new “model” package, and then annotate the functions defined within it.

One potential drawback, however, is when you need to introduce helper types or functions to model individual subprograms. In that case, these helpers could clash with existing subprograms.

[JoseRuizAdaCore]

This is also potentially very useful to specify test cases (via the Test_Case aspect). Keeping the testing part in a separate file is important because:

1. It makes the specification more readable
2. Testers are frequently different individuals from implementers or designers, so working on a different file makes sense
3. We don't usually want to modify a specification during the testing phase

[sttaft]

One potential drawback, however, is when you need to introduce helper types or functions to model individual subprograms. In that case, these helpers could clash with existing subprograms.

I had presumed that you would ignore any types or subprograms in the model package that didn't match the name/profile of a corresponding type/subprogram in the original package. But yes, you couldn't use the same name for something that didn't correspond.

[Nikokrock]

The idea of separating the model from the spec is interesting I think, but the current proposition needs to clarify a few things:

• What happens if the function already defines some aspects? Are they ignored, added? Which aspects are concerned by this feature?
• Pre/Post can be included in the final code when compiled with assertions. What is supposed to happen in that case?
• I think the current proposition will break/change the compilation model. During the compilation of the original unit there is no indication that the unit has a model. The reverse relation where you specify in the original unit the model that is used would be easier to tackle - i.e: something like Modeled_By => Math_Models.Sqrt. But it would not meet the requirement of separation of the model from the spec.

Maybe this has been proposed earlier but would adding a "dimension" to our compilation model could be the way? For example:

   --  math.ads
   package Math is
      function Sqrt (X : Float) return Float;
   end Math;

   -- math.adm
   package model Math is
       function Sqrt (X : Float) return Float
       with
          Pre  => X >= 0.0,
          Post => Sqrt'Result >= 0.0;
   end Math;

   -- match.adb
   --  ...

In such a scheme, where a separate model file is used, and if we suppose you don't need to model everything from the original spec, the main points would be the following:

• Clear separation between source and model. No need for source modification
• Different models can be easily used depending on the tooling or just the context, by simply playing with the naming package from GPRproject files
• Old compilers can still compile the code and ignore the models
• The compilation model is only "extended"

[danielmercier]

What happens if the function already defines some aspects? Are they ignored, added? Which aspects are concerned by this feature?

I agree that this needs to be clarified. From my perspective, it largely depends on the specific aspect and whether it is meant to be accumulative. For example, preconditions could be treated as a disjunction of all specified preconditions, postconditions as a conjunction, and similar rules could apply to other aspects. Essentially, we need to decide whether we want to allow aspects to accumulate on a given subprogram. If we do, then the tool must clearly define how such accumulation is handled; if not, we should explicitly disallow it—perhaps by giving the model higher precedence?

Pre/Post can be included in the final code when compiled with assertions. What is supposed to happen in that case?
I think the current proposition will break/change the compilation model. During the compilation of the original unit there is no indication that the unit has a model. The reverse relation where you specify in the original unit the model that is used would be easier to tackle - i.e: something like Modeled_By => Math_Models.Sqrt. But it would not meet the requirement of separation of the model from the spec.

What I’m proposing is to restrict the use of Model_Of to analysis tools only. While allowing the compiler to inspect models could be appealing as a way to unify semantic checks, I don’t think we should alter the runtime model—though that point is admittedly debatable.

In such a scheme, where a separate model file is used, and if we suppose you don't need to model everything from the original spec, the main points would be the following:

I hadn’t thought about this explicitly, but I was considering how to specify such packages for an analysis tool. This sounds like a very nice way to do it.