--- layout: fc_discuss_archives title: Message 37 from Frama-C-discuss on December 2011 ---
On 12/07/2011 03:36 PM, David MENTRE wrote: > Anyway, I'm just curious on how other people are using strong invariants. Hi David, Ada 2012 provides an interesting notion of strong invariants, that is only checked at certain program points: after object creation, when converting to the type, when passing an object as input parameter, or returning it as output parameter. See http://www.ada-auth.org/standards/12rm/html/RM-3-2-4.html#I1430 for more details on this "subtype predicate" feature. Here is an implementation of your code that uses it: --- procedure P is type T is record Access_Count : Natural := 0; Locked : Boolean := False; end record with Predicate => (T.Locked = (T.Access_Count > 3)); procedure Bad (V : in out T) is begin V.Access_Count := V.Access_Count + 1; V.Locked := True; end Bad; Var : T; -- predicate checked at object creation begin -- predicate checked when passing Var as input Bad (Var); -- predicate checked when returning Var as output end P; --- Just compile the code above with assertions (-gnata): $ gcc -c -gnat12 -gnata p.adb $ gnatbind p $ gnatlink p $ ./p and at run-time you get the error (placed on Bad declaration because the check is done inside Bad code for both inputs and outputs): raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : predicate failed at p.adb:8 Ada 2012 also has a notion of weak invariants, that only applies to private types defined in a package, and which are checked only on public subprograms defined in this package, on output parameters of the type. See http://www.ada-auth.org/standards/12rm/html/RM-7-3-2.html for all details. Here is your code using a type invariant: --- p.ads package P is type T is private; procedure Bad (V : in out T); private type T is record Access_Count : Natural := 0; Locked : Boolean := False; end record with Predicate => (T.Locked = (T.Access_Count > 3)); end P; --- p.adb package body P is procedure Bad (V : in out T) is begin V.Access_Count := V.Access_Count + 1; V.Locked := True; end Bad; end P; --- main.adb with P; use P; procedure Main is Var : T; begin Bad (Var); end Main; --- test.gpr project Test is for Main use ("main.adb"); package Compiler is for Default_Switches ("Ada") use ("-gnat12", "-gnata"); end Compiler; end Test; --- Compile the code using the project file above: $ gnatmake -P test $ ./main and you get a run-time exception: raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : predicate failed at p.adb:2 Of course, we plan to be able to prove both uses of subtypes predicates and type invariants statically with the tool gnatprove. Best regards, -- Yannick