From f30c3823b96782b0c2ee4f4272990bb17f894a63 Mon Sep 17 00:00:00 2001
From: Nick Treleaven <ntrel002@gmail.com>
Date: Tue, 25 Nov 2025 18:32:23 +0000
Subject: [PATCH 1/2] [spec/function] Add contract inheritance examples

---
 spec/function.dd | 59 +++++++++++++++++++++++++++++++++++++++++++++++-
 1 file changed, 58 insertions(+), 1 deletion(-)

diff --git a/spec/function.dd b/spec/function.dd
index ff58d6f83a..046aa0c4f7 100644
--- a/spec/function.dd
+++ b/spec/function.dd
@@ -378,6 +378,28 @@ $(GNAME OutStatement):
         functions then becomes a process of $(I loosening) the preconditions.
         )
 
+        $(SPEC_RUNNABLE_EXAMPLE_RUN
+        ---
+        class B
+        {
+            int i;
+
+            int f() in (i == 5) => 5;
+        }
+        class C : B
+        {
+            override int f() => i; // no `in` contract, `i` can be anything
+        }
+
+        B b = new B;
+        assert(b.i == 0);
+        //b.f(); // AssertError, `i == 5` failed
+
+        b = new C;
+        assert(b.f() == 0); // OK
+        ---
+        )
+
         $(P A function without preconditions means its precondition is always
         satisfied.
         Therefore if any
@@ -386,12 +408,47 @@ $(GNAME OutStatement):
         effect.
         )
 
+        $(SPEC_RUNNABLE_EXAMPLE_FAIL
+        ---
+        class C : Object
+        {
+            int x;
+
+            override string toString()
+            in (x > 0) // Error, Object.toString has no `in` contract
+            {
+                return "";
+            }
+        }
+        ---
+        )
+
         $(P Conversely, all of the postconditions of the function and its
-        overridden functions must to be satisfied.
+        overridden functions must be satisfied.
         Adding overriding functions then becomes a processes of $(I tightening) the
         postconditions.
         )
 
+        $(SPEC_RUNNABLE_EXAMPLE_FAIL
+        ---
+        class B
+        {
+            int i;
+
+            int f() out (; i > 5) => i;
+        }
+        class C : B
+        {
+            override int f() out (; i < 10) => i;
+        }
+
+        B b = new C;
+        b.f(); // AssertError, `i > 5` failed
+        b.i = 10;
+        b.f(); // AssertError, `i < 10` failed
+        ---
+        )
+
 
 $(H2 $(LNAME2 function-return-values, Function Return Values))
 

From 56cf3fe1cba1dadc6c39563d004588b606b411ad Mon Sep 17 00:00:00 2001
From: Nick Treleaven <ntrel002@gmail.com>
Date: Tue, 25 Nov 2025 21:30:10 +0000
Subject: [PATCH 2/2] Fix overridden postcondition wording

---
 spec/function.dd | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/spec/function.dd b/spec/function.dd
index 046aa0c4f7..664f76a4aa 100644
--- a/spec/function.dd
+++ b/spec/function.dd
@@ -388,7 +388,7 @@ $(GNAME OutStatement):
         }
         class C : B
         {
-            override int f() => i; // no `in` contract, `i` can be anything
+            override int f() => i; // no `in` contract, `i` can have any value
         }
 
         B b = new B;
@@ -423,9 +423,9 @@ $(GNAME OutStatement):
         ---
         )
 
-        $(P Conversely, all of the postconditions of the function and its
+        $(P Conversely, all the postconditions of the function and its
         overridden functions must be satisfied.
-        Adding overriding functions then becomes a processes of $(I tightening) the
+        Overriding functions then becomes a process of $(I tightening) the
         postconditions.
         )