improved layout
Isabelle_DOF/Isabelle_DOF/master This commit looks good
Details
Isabelle_DOF/Isabelle_DOF/master This commit looks good
Details
This commit is contained in:
parent
ed1143cae3
commit
6414e1e568
|
@ -463,13 +463,22 @@ doc_class EC = AC +
|
||||||
subsubsection\<open>Example: Assertions\<close>
|
subsubsection\<open>Example: Assertions\<close>
|
||||||
text\<open>Assertions are a common feature to validate properties of models, presented as a collection
|
text\<open>Assertions are a common feature to validate properties of models, presented as a collection
|
||||||
of Isabelle/HOL definitions. They are particularly relevant for highlighting corner cases of a
|
of Isabelle/HOL definitions. They are particularly relevant for highlighting corner cases of a
|
||||||
formal model.\<close>
|
formal model. For example, assume a definition: \<close>
|
||||||
|
|
||||||
definition last :: "'a list \<Rightarrow> 'a" where "last S = hd(rev S)"
|
definition last :: "'a list \<Rightarrow> 'a" where "last S = hd(rev S)"
|
||||||
|
|
||||||
|
(*<*)
|
||||||
text*[claim::assertions]\<open>For non-empty lists, our definition yields indeed the last element of a list.\<close>
|
text*[claim::assertions]\<open>For non-empty lists, our definition yields indeed the last element of a list.\<close>
|
||||||
assert*[claim::assertions] "last[4::int] = 4"
|
assert*[claim::assertions] "last[4::int] = 4"
|
||||||
assert*[claim::assertions] "last[1,2,3,4::int] = 4"
|
assert*[claim::assertions] "last[1,2,3,4::int] = 4"
|
||||||
|
(*>*)
|
||||||
|
text\<open>We want to check the consequences of this definition and can add the following sdtatements:
|
||||||
|
\begin{isar}
|
||||||
|
text*[claim::assertions]\<open>For non-empty lists, our definition yields indeed the last element of a list.\<close>
|
||||||
|
assert*[claim::assertions] "last[4::int] = 4"
|
||||||
|
assert*[claim::assertions] "last[1,2,3,4::int] = 4"
|
||||||
|
\end{isar}
|
||||||
|
\<close>
|
||||||
|
|
||||||
text\<open>As an \inlineisar+ASSERTION_ALIKES+, the \inlineisar+assertions+ class possesses a
|
text\<open>As an \inlineisar+ASSERTION_ALIKES+, the \inlineisar+assertions+ class possesses a
|
||||||
\inlineisar+properties+ attribute. The \inlineisar+assert*+ command evaluates its argument;
|
\inlineisar+properties+ attribute. The \inlineisar+assert*+ command evaluates its argument;
|
||||||
|
|
Loading…
Reference in New Issue