On Friday 13 Dec 2013 16:36:04 Stephen Leake wrote:
> In the meantime, specific examples are useful as test cases. In
> particular, I'm curious as to how you prefer to indent them. So please
> post some here; I'll add them to the tests, with "FIXME: failing -
> aspects" comments.
I guess I'll start with pre and postconditions. I suppose this would be a good
way to indent them:
procedure Foo (X : Integer;
Y : out Integer)
with Pre => X > 10 and
X < 50 and
F (X),
Post =>
Y >= X and
Some_Very_Verbose_Predicate (X, Y);
In words: align everything after the => to the column of the first non-
whitespace character? Pre and postcondition expressions generally take this
kind of form so that seems reasonable and readable to me. And here are some
basic examples of SPARK 2014 aspects in their preferred form:
procedure Swap (X, Y : in out Integer)
with Global => null,
Depends => (X => Y,
Y => X);
procedure Do_Things (X : Integer)
with Global => (Input => Foo,
In_Out => (Bar,
Baz),
Output => Bork),
Depends => (Bar =>+ X,
(Baz, Bork) => Baz);
I hope these basic examples are helpful.
While I remember, there will also be a new attribute in SPARK 2014 which looks
like this (assume for example that X is a record type with fields A, B and C):
Foo := X'Update (B => 12,
C => Y);
(This takes a copy of X and changes fields B and C.)
Thanks,
Florian
_______________________________________________
Emacs-ada-mode mailing list
[email protected]
http://host114.hostmonster.com/mailman/listinfo/emacs-ada-mode_stephe-leake.org
