RFC: Model_of aspect - #223
Conversation
9092c05 to
ed4b2a4
Compare
ed4b2a4 to
ed96937
Compare
ed96937 to
f3dc79a
Compare
|
@MartinClochardPro, please check if the validity rule on line 153 is now appropriate? I rephrased it to reference |
| ``` | ||
| decoration_unit ::= | ||
| "model" "package" package_name "is" | ||
| { decorated_subprogram_declaration } |
There was a problem hiding this comment.
The grammar only admits decorated_subprogram_declaration, is subprogram-only the intended final scope? SPARK contracts also operates on packages/types/globals. Worth a line in the RFC on whether that's in or out.
| A given subprogram may carry contracts in at most one of the main unit and the | ||
| sidecar unit. If both files supply a pre- or postcondition for the same | ||
| subprogram, the model decorator tool reports an error indicating the conflicting | ||
| line in each file. This rule prevents silent shadowing of production contracts | ||
| by sidecar contracts. |
There was a problem hiding this comment.
I think this contradict what's stated at lines 157-159.
| function Sqrt (X : Float) return Float | ||
| --# @Source_Reference@ 3 "my_math_models.ads" 1 | ||
| with | ||
| --# @Source_Reference@ 5 "my_math_models.ads" |
There was a problem hiding this comment.
Shouldn't line number be 4 here (and therefore no marker at all)?
| Post => Sqrt'Result >= 0.0; | ||
| --# @Source_Reference@ 3 "my_math.ads" 2 | ||
| function Log (X : Float) return Float; | ||
| end My_Math; |
There was a problem hiding this comment.
Is it expected that the private part of my_math.ads is missing from this unit?
| line in each file. This rule prevents silent shadowing of production contracts | ||
| by sidecar contracts. | ||
|
|
||
| If a sidecar unit exists for a package without a corresponding main source |
There was a problem hiding this comment.
This feels counter intuitive: the feature is meant to stay "read-only" on the sources I guess, so creating a unit here seems odd. Why not make it a hard error instead? Reconstructing a spec from its contracts also looks non-trivial?
| -- additional included packages | ||
| with Helper_Package; use Helper_Package; | ||
|
|
||
| model package My_Math is |
There was a problem hiding this comment.
The model keyword distinguishes decorated declarations from the ones copied through verbatim, but that could be an aspect instead of new vocabulary:
function Pow (X, Y : Float) return Float
with Model, Pre => Greater_Than (X, 0.0), Post => Greater_Than (Pow'Result, 0.0);This reuses Ada's existing aspect grammar (no new keyword, no new gramme rule,…), and would greatly simplify tooling: libadalang could parse sidecar units with its normal grammar, and LKQL rules and IDE support (navigation, completion, highlighting) would work out of the box.
It would also read better when decorating an entity that is itself named Model:
model procedure Model with …
-- vs.
procedure Model with Model, …| and define a helper function in the model package: | ||
|
|
||
| ```ada | ||
| -- my_math_models.adb (sidecar body, not compiled by the regular build) |
There was a problem hiding this comment.
The RFC doesn't define a naming convention for the model unit files. Could it either define one or state explicitly that naming is unconstrained? This also brings gprbuild support into play: how sidecar units are linked to their Ada specifications, and how they are kept out of the build.
I would propose .adm: it keeps the same base name as the spec/body, and makes clear that it isn't Ada code. gprbuild could likely handle that easily, extending the existing naming attributes accordingly.
| decoration_aspect_list ::= | ||
| decoration_aspect { "," decoration_aspect } | ||
|
|
||
| decoration_aspect ::= |
There was a problem hiding this comment.
I think the original issue for that feature wasn't limited to SPARK aspects: #197. In particular, the GNAT SAS team is interested in taint aspects. The rule should be generalized to all aspects that have no effect on execution, not just the SPARK ones.
4 participants
No description provided.