Update CENELEC_50128 theory

An application condition should be an assumption
This commit is contained in:
Nicolas Méric 2022-03-18 17:00:06 +01:00
parent a950142749
commit 2886f7df99
2 changed files with 8 additions and 4 deletions

View File

@ -373,10 +373,6 @@ doc_class FnI = requirement +
is_concerned :: "role set" <= "UNIV"
type_synonym functions_and_interfaces = FnI
doc_class AC = requirement +
is_concerned :: "role set" <= "UNIV"
type_synonym application_conditions = AC
text\<open>The category \<^emph>\<open>assumption\<close> is used for domain-specific assumptions. It has formal, semi-formal
and informal sub-categories. They have to be tracked and discharged by appropriate
@ -387,6 +383,12 @@ datatype ass_kind = informal | semiformal | formal
doc_class assumption = requirement +
assumption_kind :: ass_kind <= informal
doc_class AC = assumption +
is_concerned :: "role set" <= "UNIV"
type_synonym application_conditions = AC
text\<open> The category \<^emph>\<open>exported constraint\<close> (or \<^emph>\<open>EC\<close> for short) is used for formal application
conditions; They represent in particular \<^emph>\<open>derived constraints\<close>, i.e. constraints that arrive
as side-conditions during refinement proofs or implementation decisions and must be tracked.\<close>

View File

@ -71,6 +71,7 @@
,CENELEC_50128.SRAC.formal_repr=%
,CENELEC_50128.SRAC.assumption_kind=%
,CENELEC_50128.EC.assumption_kind=%
,CENELEC_50128.assumption.assumption_kind=%
][1]{%
\begin{isamarkuptext}%
\ifthenelse{\equal{\commandkey{CENELEC_50128.requirement.long_name}}{}}{%
@ -123,6 +124,7 @@
,CENELEC_50128.SRAC.formal_repr=%
,CENELEC_50128.SRAC.assumption_kind=%
,CENELEC_50128.EC.assumption_kind=%
,CENELEC_50128.assumption.assumption_kind=%
][1]{%
\begin{isamarkuptext}%
\ifthenelse{\equal{\commandkey{CENELEC_50128.requirement.long_name}}{}}{%