Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity

Add test of invariants of an inherited attribute of an attribute
ci/woodpecker/push/build Pipeline failed Details

This commit is contained in:
Nicolas Méric 2023-01-18 19:11:48 +01:00
parent 8fdaafa295
commit 1379f8a671
1 changed files with 11 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
src/tests/High_Level_Syntax_Invariants.thy
View File

@ -61,9 +61,19 @@ doc_class inv_test2 =
doc_class inv_test3 = inv_test1 +
b :: "inv_test1"
c:: int
invariant inv_test3 :: "a \<sigma> = 1"
invariant inv_test3 :: "a \<sigma> = 2"
invariant inv_test3' :: "a (b \<sigma>) = 2"
doc_class inv_test4 = inv_test2 +
d :: "inv_test3"
invariant inv_test4 :: "a (inv_test2.b \<sigma>) = 2"
invariant inv_test4' :: "a (d \<sigma>) = 2"
text*[inv_test1_instance::inv_test1, a=2]\<open>\<close>
text*[inv_test3_instance::inv_test3, a=2, b="@{inv-test1 \<open>inv_test1_instance\<close>}" ]\<open>\<close>
text*[inv_test4_instance::inv_test4, b="@{inv-test1 \<open>inv_test1_instance\<close>}"
, c=1, d="@{inv-test3 \<open>inv_test3_instance\<close>}"]\<open>\<close>
text\<open>To support invariant on attributes in attributes
and invariant on attributes of the superclasses,
we check that the type of the attribute of the subclass is ground:\<close>