CONTEXT RAP IN ENGLISH LATEX
INCLUDE "ISdocumentation.adl"
INCLUDE "IS.ifc"
INCLUDE "IS.pop"


PATTERN "Information Systems"
RELATION characteristic[Rule*Expression] [UNI,TOT] PRAGMA "The characteristic expression of rule ``" "'' is "
MEANING "Every rule has a {\\em characteristic expression}, which is meant to remain true across changing states. We say that a rule is true whenever its characteristic expression can be evaluated to true."
RELATION exp[Query*Expression] [UNI,TOT]
MEANING "Each query evaluates a given expression in a given state, and produces a number of facts as a result."
RELATION signature[Expression*Expression] [UNI,TOT,TRN]
MEANING "Every expression has a signature (sometimes called type)."
RELATION state[Query*State] [UNI,TOT]
MEANING "Every query operates on a state, in which expressions can be evaluated."
RELATION true[Query*Query] [PROP]
MEANING "In order to say that a query has produced `true' as a result, we will call that query  `true'."
RELATION result[Query*Statement]
MEANING "When mentioning the result of executing a query, we mean the set of facts that was produced by executing that query."
RELATION sat[State*Rule]
MEANING "It makes sense to say that a state satisfies a rule, meaning that the rule is true in that state."
RELATION pred[State*State] [UNI,IRF]
MEANING "Each state except the initial state will have a predecessor. Two states that have the same predecessor are the same."
RELATION equivalued[Query*Query] [RFX,TRN,ASY]
MEANING "We shall use the word equivalued to indicate that executing two queries in the same state has produced identical results."

CLASSIFY Expression ISA Statement

RULE "def equivalued" : equivalued = state;state~ /\ result<>result~
MEANING "Two queries are called equivalued if they produce exactly the same facts from the same state."

RULE "def sat" : sat = state~;true;exp;characteristic~
MEANING "For a rule $r$ to satisfy a state $s$ means: the query that executes the rule expression of rule $r$ yields true."

RULE "def true" : true = exp;signature;exp~;equivalued
MEANING "A query is true if it is equivalued with a query of the signature of its expression. I.e. its execution yields the same set of facts as does the signature executed on the same state."

IDENT query : Query(exp, state)

IDENT state : State(pred)

ENDPATTERN

PATTERN "Documentation"
RELATION meaning[Concept*NatLang]
MEANING "It makes sense to talk about the meaning of a concept. The meaning is a written statement in natural language."
RULE conceptHasMeaning : I[Concept] |- meaning;meaning~
MEANING "Every concept has a meaning"

RELATION purpose[Concept*NatLang]
MEANING "It makes sense to talk about the purpose of a concept. The purpose is a written statement in natural language."
RULE conceptHasPurpose : I[Concept] |- purpose;purpose~
MEANING "Every concept must have a purpose, written in natural language."

RELATION reference[Concept*Reference]
MEANING "A concept that originates from a written source can be referenced. The link between concept and reference makes it traceable."
RULE conceptHasReference : I[Concept] |- reference;reference~
MEANING "Every concept must be traceable to its origin(s)."

RELATION meaning[Relation*NatLang]
MEANING "It makes sense to talk about the meaning of a relation. The meaning is a written statement in natural language."
RULE relationHasMeaning : I[Relation] |- meaning;meaning~
MEANING "Every relation has a meaning"

RELATION purpose[Relation*NatLang]
MEANING "It makes sense to talk about the purpose of a relation. The purpose is a written statement in natural language."
RULE relationHasPurpose : I[Relation] |- purpose;purpose~
MEANING "Every relation must have a purpose, written in natural language."

RELATION reference[Relation*Reference]
MEANING "A relation that originates from a written source can be referenced. The link between relation and reference makes it traceable."
RULE relationHasReference : I[Relation] |- reference;reference~
MEANING "Every relation must be traceable to its origin(s)."

RELATION meaning[Rule*NatLang]
MEANING "It makes sense to talk about the meaning of a rule. The meaning is a written statement in natural language."
RULE ruleHasMeaning : I[Rule] |- meaning;meaning~
MEANING "Every rule has a meaning"

RELATION purpose[Rule*NatLang]
MEANING "It makes sense to talk about the purpose of a rule. The purpose is a written statement in natural language."
RULE ruleHasPurpose : I[Rule] |- purpose;purpose~
MEANING "Every rule must have a purpose, written in natural language."

RELATION reference[Rule*Reference]
MEANING "A rule that originates from a written source can be referenced. The link between rule and reference makes it traceable."
RULE ruleHasReference : I[Rule] |- reference;reference~
MEANING "Every rule must be traceable to its origin(s)."
ENDPATTERN

PATTERN "Enforcement"
CONCEPT EnforcementType "Rules can be enforced either by humans or by computers. An enforcement type is used to distinguish between the two."
CONCEPT RuleEnforcement "A rule can be enforced within a context, which means it is being kept without violations."
RULE enforcementType : I[EnforcementType] = 'Human' \/ 'Computer'
RELATION enforcement[RuleEnforcement*EnforcementType] [UNI,TOT]
MEANING "For each rule enforcement, a way of enforcement is defined."
RELATION rule[RuleEnforcement*Rule] [TOT]
MEANING "The rule(s) being enforced are linked to the rule enforcement."
RELATION valid[RuleEnforcement*Context] [TOT]
MEANING "We can say that a rule is valid in a context, which means that the rule should not have any violations in that context."
ENDPATTERN


ENDCONTEXT