Reflect the abstract type scenario more precisely in LRM

language-reference-manual/lrm.trlc

@@ -656,21 +656,19 @@ section "Type declarations" {
       text = "The root type for a record extension must be a valid record type."
     }
 
-    Static_Semantics Abstract_Type_Declaration {
-      text = '''
-        A record may be marked `abstract`.
-      '''
-    }
-
     Static_Semantics Abstract_Types {
       text = '''
-        If a record is marked `abstract`, then no objects of this
+        A record may be marked `abstract`, in which case no objects of this
         type may be declared. It must be extended *(even if that extension is
         empty)* before instances of that type can be declared.
         *(Note that it is possible to have components of an abstract type.)*
       '''
     }
 
+    Recommendation Abstract_Type_Not_Extended {
+      text = '''It is recommended to emit a warning if an abstract type is not extended.'''
+    }
+
     Static_Semantics Final_Types {
       text = '''
         A record may be marked `final`, and the extension of a `final` type

tests-system/rbt-abstract-types-1/abstract.rsl

@@ -0,0 +1,6 @@
+package Ant_house
+
+//Expectation: An error is emitted because an object of this abstract type is created in trlc
+abstract type Ant {
+  desc String
+}

tests-system/rbt-abstract-types-1/abstract.trlc

@@ -0,0 +1,5 @@
+package Ant_house
+
+Ant willy{
+    desc = "It is forbidden to create an object of an abstract type"
+}

tests-system/rbt-abstract-types-1/output

@@ -0,0 +1,5 @@
+abstract type Ant {
+              ^^^ rbt-abstract-types-1/abstract.rsl:4: issue: abstract type Ant does not have any extensions [abstract_leaf_types]
+Ant willy{
+^^^ rbt-abstract-types-1/abstract.trlc:3: error: cannot declare object of abstract record type Ant
+Processed 1 model and 1 requirement file and found 1 warning and 1 error

tests-system/rbt-abstract-types-1/output.brief

@@ -0,0 +1,2 @@
+rbt-abstract-types-1/abstract.trlc:3:1: trlc error: cannot declare object of abstract record type Ant
+Processed 1 model and 1 requirement file and found 1 error

tests-system/rbt-abstract-types-1/output.json

@@ -0,0 +1,3 @@
+Ant willy{
+^^^ rbt-abstract-types-1/abstract.trlc:3: error: cannot declare object of abstract record type Ant
+Processed 1 model and 1 requirement file and found 1 error

tests-system/rbt-abstract-types-1/output.smtlib

@@ -0,0 +1,5 @@
+abstract type Ant {
+              ^^^ rbt-abstract-types-1/abstract.rsl:4: issue: abstract type Ant does not have any extensions [abstract_leaf_types]
+Ant willy{
+^^^ rbt-abstract-types-1/abstract.trlc:3: error: cannot declare object of abstract record type Ant
+Processed 1 model and 1 requirement file and found 1 warning and 1 error

tests-system/rbt-abstract-types-not-extended/abstract.rsl

@@ -0,0 +1,6 @@
+package Ant_house
+
+//Expectation: A warning should be emitted as abstract type is not extended
+abstract type Ant {
+  x Integer
+}

tests-system/rbt-abstract-types-not-extended/output

@@ -0,0 +1,3 @@
+abstract type Ant {
+              ^^^ rbt-abstract-types-not-extended/abstract.rsl:4: issue: abstract type Ant does not have any extensions [abstract_leaf_types]
+Processed 1 model and 0 requirement files and found 1 warning

tests-system/rbt-abstract-types-not-extended/output.brief

@@ -0,0 +1 @@
+Processed 1 model and 0 requirement files and found no issues

tests-system/rbt-abstract-types-not-extended/output.json

@@ -0,0 +1,2 @@
+{}
+Processed 1 model and 0 requirement files and found no issues

tests-system/rbt-abstract-types-not-extended/output.smtlib

@@ -0,0 +1,3 @@
+abstract type Ant {
+              ^^^ rbt-abstract-types-not-extended/abstract.rsl:4: issue: abstract type Ant does not have any extensions [abstract_leaf_types]
+Processed 1 model and 0 requirement files and found 1 warning

tests-system/rbt-abstract-types/abstract.rsl

@@ -0,0 +1,11 @@
+package Ant_house
+
+//Expectation: No warning and no error
+//Hence, this test also verifies the non-error scenario of Abstract_Type_Not_Extended
+abstract type Ant {
+  x Integer
+}
+
+type Ant_hill extends Ant {
+  desc String
+}

tests-system/rbt-abstract-types/output

@@ -0,0 +1 @@
+Processed 1 model and 0 requirement files and found no issues

tests-system/rbt-abstract-types/output.brief

@@ -0,0 +1 @@
+Processed 1 model and 0 requirement files and found no issues

tests-system/rbt-abstract-types/output.json

@@ -0,0 +1,2 @@
+{}
+Processed 1 model and 0 requirement files and found no issues

tests-system/rbt-abstract-types/output.smtlib

@@ -0,0 +1 @@
+Processed 1 model and 0 requirement files and found no issues

trlc/lint.py

@@ -52,13 +52,13 @@ def perform_sanity_checks(self):
                     ok = False
 
         # Complain about abstract types without extensions
+        # lobster-trace: LRM.Abstract_Type_Not_Extended
         for package in self.stab.values(ast.Package):
             for n_typ in package.symbols.values(ast.Record_Type):
                 if n_typ.is_abstract and not self.abstract_extensions[n_typ]:
                     self.mh.check(
                         n_typ.location,
-                        "abstract type %s does not have any extensions" %
-                        n_typ.name,
+                        f"abstract type {n_typ.name} does not have any extensions",
                         "abstract_leaf_types")
 
         return ok

trlc/parser.py

@@ -616,7 +616,6 @@ def parse_record_declaration(self):
         t_final     = None
         is_abstract = False
         is_final    = False
-        # lobster-trace: LRM.Abstract_Type_Declaration
         if self.peek_kw("abstract"):
             self.match_kw("abstract")
             t_abstract  = self.ct