diff --git a/language-reference-manual/lrm.trlc b/language-reference-manual/lrm.trlc index d62bbbc..3b8cb68 100644 --- a/language-reference-manual/lrm.trlc +++ b/language-reference-manual/lrm.trlc @@ -1519,8 +1519,8 @@ section "Quantification" { Grammar Quantified_Expression { bnf = ''' quantified_expression ::= - quantifier IDENTIFIER_name 'in' IDENTIFIER_component_name '=>' - expression_PREDICATE + '(' quantifier IDENTIFIER_name 'in' IDENTIFIER_component_name '=>' + expression_PREDICATE ')' quantifier ::= 'forall' | 'exists' ''' @@ -1546,14 +1546,6 @@ section "Quantification" { quantified expression is Boolean.''' } - Dynamic_Semantics Quantification_Evaluation { - text = '''During evaluation of the quantified expression, each element - of the array is evaluated in sequence and its - value is bound to the declared name. The - predicated is then evaluated with this - binding.''' - } - Dynamic_Semantics Universal_Quantification_Semantics { text = '''For universal *(forall)* quantification the final value is true iff all predicates evaluate to @@ -1569,6 +1561,14 @@ section "Quantification" { vacuously false.)*''' } + Note Quantification_Evaluation { + text = '''During evaluation of the quantified expression, each element + of the array is evaluated in sequence and its + value is bound to the declared name. The + predicated is then evaluated with this + binding.''' + } + Recommendation Quantification_Short_Circuit_Evaluation { text = '''In general Quantification is equivalent to a chain of `and` or `or` expressions, however it is left @@ -1580,6 +1580,7 @@ section "Quantification" { '''For static analysis or linting, use non-short-circuit semantics, as using a quantifier as a complex guard is not reasonable.'''] + untraced_reason = "Non-normative text" } } diff --git a/tests-system/rbt-existential-quantification-semantics/foo.rsl b/tests-system/rbt-existential-quantification-semantics/foo.rsl new file mode 100644 index 0000000..0a87a98 --- /dev/null +++ b/tests-system/rbt-existential-quantification-semantics/foo.rsl @@ -0,0 +1,9 @@ +package Foo + +type T { + a Integer[0..*] +} + +checks T { + (exists item in a => item == 7), warning "there is no 7 in a" +} diff --git a/tests-system/rbt-existential-quantification-semantics/foo.trlc b/tests-system/rbt-existential-quantification-semantics/foo.trlc new file mode 100644 index 0000000..982fa64 --- /dev/null +++ b/tests-system/rbt-existential-quantification-semantics/foo.trlc @@ -0,0 +1,9 @@ +package Foo + +T Bar { + a = [7] +} + +T Kitten { + a = [] +} diff --git a/tests-system/rbt-existential-quantification-semantics/output b/tests-system/rbt-existential-quantification-semantics/output new file mode 100644 index 0000000..26da7f5 --- /dev/null +++ b/tests-system/rbt-existential-quantification-semantics/output @@ -0,0 +1,3 @@ +T Kitten { + ^^^^^^ rbt-existential-quantification-semantics/foo.trlc:7: check warning: there is no 7 in a +Processed 1 model and 1 requirement file and found 1 warning diff --git a/tests-system/rbt-existential-quantification-semantics/output.brief b/tests-system/rbt-existential-quantification-semantics/output.brief new file mode 100644 index 0000000..0f28ec1 --- /dev/null +++ b/tests-system/rbt-existential-quantification-semantics/output.brief @@ -0,0 +1 @@ +rbt-existential-quantification-semantics/foo.trlc:7:3: trlc check warning: there is no 7 in a diff --git a/tests-system/rbt-existential-quantification-semantics/output.json b/tests-system/rbt-existential-quantification-semantics/output.json new file mode 100644 index 0000000..fa198fd --- /dev/null +++ b/tests-system/rbt-existential-quantification-semantics/output.json @@ -0,0 +1,13 @@ +T Kitten { + ^^^^^^ rbt-existential-quantification-semantics/foo.trlc:7: check warning: there is no 7 in a +{ + "Bar": { + "a": [ + 7 + ] + }, + "Kitten": { + "a": [] + } +} +Processed 1 model and 1 requirement file and found 1 warning diff --git a/tests-system/rbt-existential-quantification-semantics/output.smtlib b/tests-system/rbt-existential-quantification-semantics/output.smtlib new file mode 100644 index 0000000..26da7f5 --- /dev/null +++ b/tests-system/rbt-existential-quantification-semantics/output.smtlib @@ -0,0 +1,3 @@ +T Kitten { + ^^^^^^ rbt-existential-quantification-semantics/foo.trlc:7: check warning: there is no 7 in a +Processed 1 model and 1 requirement file and found 1 warning diff --git a/tests-system/rbt-quantification-naming-scope/foo.rsl b/tests-system/rbt-quantification-naming-scope/foo.rsl new file mode 100644 index 0000000..c8ba931 --- /dev/null +++ b/tests-system/rbt-quantification-naming-scope/foo.rsl @@ -0,0 +1,11 @@ +package Foo + +type T { + a Integer[1..10] +} + +checks T { + (forall item in a => item > 0), warning "All items must be positive" + (forall item in a => item < 10), warning "All items must be less than 10" + (forall a in a => a != 7), warning "No sevens allowed" +} diff --git a/tests-system/rbt-quantification-naming-scope/output b/tests-system/rbt-quantification-naming-scope/output new file mode 100644 index 0000000..2e42ad4 --- /dev/null +++ b/tests-system/rbt-quantification-naming-scope/output @@ -0,0 +1,3 @@ +(forall a in a => a != 7), warning "No sevens allowed" + ^ rbt-quantification-naming-scope/foo.rsl:10: error: shadows Composite_Component a from foo.rsl:4 +Processed 1 model and 0 requirement files and found 1 error diff --git a/tests-system/rbt-quantification-naming-scope/output.brief b/tests-system/rbt-quantification-naming-scope/output.brief new file mode 100644 index 0000000..f3a7920 --- /dev/null +++ b/tests-system/rbt-quantification-naming-scope/output.brief @@ -0,0 +1 @@ +rbt-quantification-naming-scope/foo.rsl:10:13: trlc error: shadows Composite_Component a from foo.rsl:4 diff --git a/tests-system/rbt-quantification-naming-scope/output.json b/tests-system/rbt-quantification-naming-scope/output.json new file mode 100644 index 0000000..2e42ad4 --- /dev/null +++ b/tests-system/rbt-quantification-naming-scope/output.json @@ -0,0 +1,3 @@ +(forall a in a => a != 7), warning "No sevens allowed" + ^ rbt-quantification-naming-scope/foo.rsl:10: error: shadows Composite_Component a from foo.rsl:4 +Processed 1 model and 0 requirement files and found 1 error diff --git a/tests-system/rbt-quantification-naming-scope/output.smtlib b/tests-system/rbt-quantification-naming-scope/output.smtlib new file mode 100644 index 0000000..2e42ad4 --- /dev/null +++ b/tests-system/rbt-quantification-naming-scope/output.smtlib @@ -0,0 +1,3 @@ +(forall a in a => a != 7), warning "No sevens allowed" + ^ rbt-quantification-naming-scope/foo.rsl:10: error: shadows Composite_Component a from foo.rsl:4 +Processed 1 model and 0 requirement files and found 1 error diff --git a/tests-system/rbt-quantification-object-1/foo.rsl b/tests-system/rbt-quantification-object-1/foo.rsl new file mode 100644 index 0000000..6d5ff00 --- /dev/null +++ b/tests-system/rbt-quantification-object-1/foo.rsl @@ -0,0 +1,9 @@ +package Foo + +type Potato { + a String +} + +checks Potato { + (forall char in a => char != "a"), warning "a should not contain the letter a" +} diff --git a/tests-system/rbt-quantification-object-1/output b/tests-system/rbt-quantification-object-1/output new file mode 100644 index 0000000..f1014cb --- /dev/null +++ b/tests-system/rbt-quantification-object-1/output @@ -0,0 +1,3 @@ +(forall char in a => char != "a"), warning "a should not contain the letter a" + ^ rbt-quantification-object-1/foo.rsl:8: error: you can only quantify over arrays +Processed 1 model and 0 requirement files and found 1 error diff --git a/tests-system/rbt-quantification-object-1/output.brief b/tests-system/rbt-quantification-object-1/output.brief new file mode 100644 index 0000000..979f63e --- /dev/null +++ b/tests-system/rbt-quantification-object-1/output.brief @@ -0,0 +1 @@ +rbt-quantification-object-1/foo.rsl:8:21: trlc error: you can only quantify over arrays diff --git a/tests-system/rbt-quantification-object-1/output.json b/tests-system/rbt-quantification-object-1/output.json new file mode 100644 index 0000000..f1014cb --- /dev/null +++ b/tests-system/rbt-quantification-object-1/output.json @@ -0,0 +1,3 @@ +(forall char in a => char != "a"), warning "a should not contain the letter a" + ^ rbt-quantification-object-1/foo.rsl:8: error: you can only quantify over arrays +Processed 1 model and 0 requirement files and found 1 error diff --git a/tests-system/rbt-quantification-object-1/output.smtlib b/tests-system/rbt-quantification-object-1/output.smtlib new file mode 100644 index 0000000..f1014cb --- /dev/null +++ b/tests-system/rbt-quantification-object-1/output.smtlib @@ -0,0 +1,3 @@ +(forall char in a => char != "a"), warning "a should not contain the letter a" + ^ rbt-quantification-object-1/foo.rsl:8: error: you can only quantify over arrays +Processed 1 model and 0 requirement files and found 1 error diff --git a/tests-system/rbt-quantification-object-2/foo.rsl b/tests-system/rbt-quantification-object-2/foo.rsl new file mode 100644 index 0000000..81ab03e --- /dev/null +++ b/tests-system/rbt-quantification-object-2/foo.rsl @@ -0,0 +1,9 @@ +package Foo + +type Potato { + a String +} + +checks Potato { + (forall char in b => char != "a"), warning "b should not contain the letter a" +} diff --git a/tests-system/rbt-quantification-object-2/output b/tests-system/rbt-quantification-object-2/output new file mode 100644 index 0000000..c9019dd --- /dev/null +++ b/tests-system/rbt-quantification-object-2/output @@ -0,0 +1,3 @@ +(forall char in b => char != "a"), warning "b should not contain the letter a" + ^ rbt-quantification-object-2/foo.rsl:8: error: unknown symbol b +Processed 1 model and 0 requirement files and found 1 error diff --git a/tests-system/rbt-quantification-object-2/output.brief b/tests-system/rbt-quantification-object-2/output.brief new file mode 100644 index 0000000..5688779 --- /dev/null +++ b/tests-system/rbt-quantification-object-2/output.brief @@ -0,0 +1 @@ +rbt-quantification-object-2/foo.rsl:8:21: trlc error: unknown symbol b diff --git a/tests-system/rbt-quantification-object-2/output.json b/tests-system/rbt-quantification-object-2/output.json new file mode 100644 index 0000000..c9019dd --- /dev/null +++ b/tests-system/rbt-quantification-object-2/output.json @@ -0,0 +1,3 @@ +(forall char in b => char != "a"), warning "b should not contain the letter a" + ^ rbt-quantification-object-2/foo.rsl:8: error: unknown symbol b +Processed 1 model and 0 requirement files and found 1 error diff --git a/tests-system/rbt-quantification-object-2/output.smtlib b/tests-system/rbt-quantification-object-2/output.smtlib new file mode 100644 index 0000000..c9019dd --- /dev/null +++ b/tests-system/rbt-quantification-object-2/output.smtlib @@ -0,0 +1,3 @@ +(forall char in b => char != "a"), warning "b should not contain the letter a" + ^ rbt-quantification-object-2/foo.rsl:8: error: unknown symbol b +Processed 1 model and 0 requirement files and found 1 error diff --git a/tests-system/rbt-quantified-expression/foo.rsl b/tests-system/rbt-quantified-expression/foo.rsl new file mode 100644 index 0000000..d877e16 --- /dev/null +++ b/tests-system/rbt-quantified-expression/foo.rsl @@ -0,0 +1,11 @@ +package Foo + +type T { + a Integer[1..*] +} + +checks T { + (forall item in a => item > 0), warning "All items must be positive", a + (exists item in a => item == 7), warning "7 is a lucky number", a + (forall item in a => 42), warning "All items must be positive", a +} diff --git a/tests-system/rbt-quantified-expression/foo.trlc b/tests-system/rbt-quantified-expression/foo.trlc new file mode 100644 index 0000000..3f3e23c --- /dev/null +++ b/tests-system/rbt-quantified-expression/foo.trlc @@ -0,0 +1,5 @@ +package Foo + +T Bar { + a = [1, 2, 3, 7] +} diff --git a/tests-system/rbt-quantified-expression/output b/tests-system/rbt-quantified-expression/output new file mode 100644 index 0000000..cd5ef1e --- /dev/null +++ b/tests-system/rbt-quantified-expression/output @@ -0,0 +1,3 @@ +(forall item in a => 42), warning "All items must be positive", a + ^^ rbt-quantified-expression/foo.rsl:10: error: expected expression of type Builtin_Boolean, got Builtin_Integer instead +Processed 1 model and 1 requirement file and found 1 error diff --git a/tests-system/rbt-quantified-expression/output.brief b/tests-system/rbt-quantified-expression/output.brief new file mode 100644 index 0000000..d16c813 --- /dev/null +++ b/tests-system/rbt-quantified-expression/output.brief @@ -0,0 +1 @@ +rbt-quantified-expression/foo.rsl:10:26: trlc error: expected expression of type Builtin_Boolean, got Builtin_Integer instead diff --git a/tests-system/rbt-quantified-expression/output.json b/tests-system/rbt-quantified-expression/output.json new file mode 100644 index 0000000..cd5ef1e --- /dev/null +++ b/tests-system/rbt-quantified-expression/output.json @@ -0,0 +1,3 @@ +(forall item in a => 42), warning "All items must be positive", a + ^^ rbt-quantified-expression/foo.rsl:10: error: expected expression of type Builtin_Boolean, got Builtin_Integer instead +Processed 1 model and 1 requirement file and found 1 error diff --git a/tests-system/rbt-quantified-expression/output.smtlib b/tests-system/rbt-quantified-expression/output.smtlib new file mode 100644 index 0000000..cd5ef1e --- /dev/null +++ b/tests-system/rbt-quantified-expression/output.smtlib @@ -0,0 +1,3 @@ +(forall item in a => 42), warning "All items must be positive", a + ^^ rbt-quantified-expression/foo.rsl:10: error: expected expression of type Builtin_Boolean, got Builtin_Integer instead +Processed 1 model and 1 requirement file and found 1 error diff --git a/tests-system/rbt-quantified-expression/tracing b/tests-system/rbt-quantified-expression/tracing new file mode 100644 index 0000000..d76a7b7 --- /dev/null +++ b/tests-system/rbt-quantified-expression/tracing @@ -0,0 +1 @@ +LRM.Quantification_Type diff --git a/tests-system/rbt-universal-quantification-semantics/foo.rsl b/tests-system/rbt-universal-quantification-semantics/foo.rsl new file mode 100644 index 0000000..f2f71b5 --- /dev/null +++ b/tests-system/rbt-universal-quantification-semantics/foo.rsl @@ -0,0 +1,9 @@ +package Foo + +type T { + a Integer[0..*] +} + +checks T { + (forall item in a => item > 0), warning "All items must be positive" +} diff --git a/tests-system/rbt-universal-quantification-semantics/foo.trlc b/tests-system/rbt-universal-quantification-semantics/foo.trlc new file mode 100644 index 0000000..230875d --- /dev/null +++ b/tests-system/rbt-universal-quantification-semantics/foo.trlc @@ -0,0 +1,13 @@ +package Foo + +T Bar { + a = [-1] +} + +T Kitten { + a = [] +} + +T Potato { + a = [-1, 1] +} diff --git a/tests-system/rbt-universal-quantification-semantics/output b/tests-system/rbt-universal-quantification-semantics/output new file mode 100644 index 0000000..07661ca --- /dev/null +++ b/tests-system/rbt-universal-quantification-semantics/output @@ -0,0 +1,5 @@ +T Bar { + ^^^ rbt-universal-quantification-semantics/foo.trlc:3: check warning: All items must be positive +T Potato { + ^^^^^^ rbt-universal-quantification-semantics/foo.trlc:11: check warning: All items must be positive +Processed 1 model and 1 requirement file and found 2 warnings diff --git a/tests-system/rbt-universal-quantification-semantics/output.brief b/tests-system/rbt-universal-quantification-semantics/output.brief new file mode 100644 index 0000000..c4f34df --- /dev/null +++ b/tests-system/rbt-universal-quantification-semantics/output.brief @@ -0,0 +1,2 @@ +rbt-universal-quantification-semantics/foo.trlc:3:3: trlc check warning: All items must be positive +rbt-universal-quantification-semantics/foo.trlc:11:3: trlc check warning: All items must be positive diff --git a/tests-system/rbt-universal-quantification-semantics/output.json b/tests-system/rbt-universal-quantification-semantics/output.json new file mode 100644 index 0000000..e25ab77 --- /dev/null +++ b/tests-system/rbt-universal-quantification-semantics/output.json @@ -0,0 +1,21 @@ +T Bar { + ^^^ rbt-universal-quantification-semantics/foo.trlc:3: check warning: All items must be positive +T Potato { + ^^^^^^ rbt-universal-quantification-semantics/foo.trlc:11: check warning: All items must be positive +{ + "Bar": { + "a": [ + -1 + ] + }, + "Kitten": { + "a": [] + }, + "Potato": { + "a": [ + -1, + 1 + ] + } +} +Processed 1 model and 1 requirement file and found 2 warnings diff --git a/tests-system/rbt-universal-quantification-semantics/output.smtlib b/tests-system/rbt-universal-quantification-semantics/output.smtlib new file mode 100644 index 0000000..07661ca --- /dev/null +++ b/tests-system/rbt-universal-quantification-semantics/output.smtlib @@ -0,0 +1,5 @@ +T Bar { + ^^^ rbt-universal-quantification-semantics/foo.trlc:3: check warning: All items must be positive +T Potato { + ^^^^^^ rbt-universal-quantification-semantics/foo.trlc:11: check warning: All items must be positive +Processed 1 model and 1 requirement file and found 2 warnings diff --git a/trlc/ast.py b/trlc/ast.py index b48207f..c63d95d 100644 --- a/trlc/ast.py +++ b/trlc/ast.py @@ -2046,6 +2046,8 @@ def __init__(self, mh, location, n_variable, n_source, n_expr): + # lobster-trace: LRM.Quantified_Expression + # lobster-trace: LRM.Quantification_Type super().__init__(location, typ) assert isinstance(typ, Builtin_Boolean) assert isinstance(universal, bool) @@ -2077,6 +2079,8 @@ def to_string(self): def evaluate(self, mh, context): # lobster-trace: LRM.Null_Is_Invalid + # lobster-trace: LRM.Universal_Quantification_Semantics + # lobster-trace: LRM.Existential_Quantification_Semantics assert isinstance(mh, Message_Handler) assert context is None or isinstance(context, dict) diff --git a/trlc/parser.py b/trlc/parser.py index e80e7e4..aae52cf 100644 --- a/trlc/parser.py +++ b/trlc/parser.py @@ -1064,6 +1064,7 @@ def parse_primary(self, scope): return self.parse_name(scope) def parse_quantified_expression(self, scope): + # lobster-trace: LRM.Quantified_Expression assert isinstance(scope, ast.Scope) if self.peek_kw("forall"): @@ -1078,6 +1079,7 @@ def parse_quantified_expression(self, scope): self.match("IDENTIFIER") t_qv = self.ct if scope.contains(t_qv.value): + # lobster-trace: LRM.Quantification_Naming_Scope pdef = scope.lookup(self.mh, t_qv) self.mh.error(t_qv.location, "shadows %s %s from %s" % @@ -1092,6 +1094,7 @@ def parse_quantified_expression(self, scope): field) n_source.set_ast_link(self.ct) if not isinstance(field.n_typ, ast.Array_Type): + # lobster-trace: LRM.Quantification_Object self.mh.error(self.ct.location, "you can only quantify over arrays") n_var = ast.Quantified_Variable(t_qv.value,