This is an automated email from the ASF dual-hosted git repository.
asf-gitbox-commits pushed a commit to branch asf-site
in repository https://gitbox.apache.org/repos/asf/groovy-dev-site.git
The following commit(s) were added to refs/heads/asf-site by this push:
new c08d527 2026/05/30 12:39:49: Generated dev website from
groovy-website@e8e9fbe
c08d527 is described below
commit c08d52726d7d60b70b9257f181ff56e4c448812f
Author: jenkins <[email protected]>
AuthorDate: Sat May 30 12:39:49 2026 +0000
2026/05/30 12:39:49: Generated dev website from groovy-website@e8e9fbe
---
blog/groovy6-functional.html | 107 +++++++++++++++++++++++++++++--------------
search/search-index.json | 2 +-
2 files changed, 74 insertions(+), 35 deletions(-)
diff --git a/blog/groovy6-functional.html b/blog/groovy6-functional.html
index cdd5663..03f265a 100644
--- a/blog/groovy6-functional.html
+++ b/blog/groovy6-functional.html
@@ -63,7 +63,7 @@
</ul>
</div>
</div>
- </div><div id='content' class='page-1'><div
class='row'><div class='row-fluid'><div class='col-lg-3'><ul
class='nav-sidebar'><li><a href='./'>Blog index</a></li><li class='active'><a
href='#doc'>Groovy 6 features for Functional Programmers</a></li><li><a
href='#_introduction' class='anchor-link'>Introduction</a></li><li><a
href='#_what_groovy_already_gave_you' class='anchor-link'>What Groovy already
gave you</a></li><li><a href='#_monoids_and_semigroups_checked' c [...]
+ </div><div id='content' class='page-1'><div
class='row'><div class='row-fluid'><div class='col-lg-3'><ul
class='nav-sidebar'><li><a href='./'>Blog index</a></li><li class='active'><a
href='#doc'>Groovy 6 features for Functional Programmers</a></li><li><a
href='#_introduction' class='anchor-link'>Introduction</a></li><li><a
href='#_what_groovy_already_gave_you' class='anchor-link'>What Groovy already
gave you</a></li><li><a href='#_monoids_and_semigroups_checked' c [...]
<a href="https://github.com/paulk-asert/"; target="_blank" rel="noopener
noreferrer"><img style="border-radius:50%;height:48px;width:auto"
src="img/paulk-asert.png" alt="Paul King"></a>
<div style="display:grid;align-items:center;margin:0.1ex;padding:0ex">
<div><a href="https://github.com/paulk-asert/"; target="_blank" rel="noopener
noreferrer"><span>Paul King</span></a></div>
@@ -1109,7 +1109,7 @@ Groovy team uses to build the in-tree checkers.</p>
</div>
</div>
<div class="sect1">
-<h2
id="_from_contract_grade_to_proof_grade_an_smt_backed_precondition_checker">From
contract-grade to proof-grade: an SMT-backed precondition checker</h2>
+<h2
id="_from_contract_grade_to_proof_grade_an_smt_backed_precondition_and_postcondition_checker">From
contract-grade to proof-grade: an SMT-backed precondition and postcondition
checker</h2>
<div class="sectionbody">
<div class="paragraph">
<p>The previous demo wrote a <strong>structural</strong> checker — names,
arity, field
@@ -1134,11 +1134,14 @@ the call site. Dafny and OpenJML close that gap with an
SMT solver.</p>
<div class="paragraph">
<p>Here is the part that might be surprising: for a tractable fragment, you can
close it in Groovy <strong>today</strong> — no compiler change, no GEP — by
putting a
-solver behind a type-checking extension. The spike below scopes itself
-to exactly one check (preconditions) over one fragment (linear integer
-arithmetic, comparisons, and booleans). Anything outside that fragment
-is reported as a loud "skipped", never a silent pass — OpenJML’s
-ESC-mode discipline, kept honest.</p>
+solver behind a type-checking extension. The spike below covers two of
+those checks (preconditions and postconditions) over one fragment
+(linear integer arithmetic, comparisons, and booleans). Anything
+outside that fragment is reported as a loud "skipped", never a silent
+pass — OpenJML’s ESC-mode discipline, kept honest.</p>
+</div>
+<div class="paragraph">
+<p>Let’s start by exploring preconditions.</p>
</div>
<div class="sect2">
<h3 id="_producer_side_2">Producer side</h3>
@@ -1257,18 +1260,53 @@ contradictory <code>if (n < 0) isqrt(n)</code>
(<code>n = -1</code>).</p>
</div>
</div>
<div class="sect2">
+<h3 id="_postconditions_too">Postconditions, too</h3>
+<div class="paragraph">
+<p>The same machinery checks <code>@Ensures</code> postconditions — proving
what a
+method <strong>returns</strong>, not just what its callers pass. The one
structural
+difference is that a postcondition is verified against the method’s own
+body, so the class declaring it is itself <code>@TypeChecked</code>. A wrong
+result is refuted just like a precondition, with the values that break
+it:</p>
+</div>
+<div class="listingblock">
+<div class="content">
+<pre class="prettyprint highlight"><code data-lang="groovy">@Ensures({ result
>= a && result >= b })
+static int max(int a, int b) {
+ if (a > b) b else a // returns the wrong branch
+}</code></pre>
+</div>
+</div>
+<div class="listingblock">
+<div class="content">
+<pre class="prettyprint highlight"><code>[Static type checking] - Cannot prove
postcondition of max holds on this return path
+ ensured: ((result >= a) && (result >= b))
+ counterexample: a = 0, b = 1</code></pre>
+</div>
+</div>
+<div class="paragraph">
+<p>Swap the branches back to <code>if (a > b) a else b</code> and it
verifies. The
+checker walks every execution path of the body — straight-line code,
+<code>if</code>/<code>else</code>, single-assignment locals — and discharges
the obligation
+on each; the companion repo’s
<code>MinMax</code>/<code>BadEnsures</code> carry the worked
+examples.</p>
+</div>
+</div>
+<div class="sect2">
<h3 id="_whats_checked_what_isnt_2">What’s checked, what isn’t</h3>
<div class="paragraph">
-<p>Same honesty as the wire demo. The checker reasons about the
<strong>argument
-expression</strong> and the <strong>enclosing <code>if</code> guards</strong>,
and nothing else. It does
-not symbolically execute the method body, so an intermediate local —
-<code>int sq = k * 1; isqrt(sq)</code> — is outside scope: <code>sq</code> is
an
-unconstrained variable as far as the call site is concerned. Anything
-beyond the linear-integer fragment (division, method calls, arrays,
-quantifiers) is reported as skipped, loudly, rather than waved through.
-That is the same trade made throughout this post: flow-sensitive work
-lives outside the type system, declarations carry the contract, and
-the type stays simple while the checker does the work.</p>
+<p>Same honesty as the wire demo, and the scope differs by mode. At a
+<strong>call site</strong>, the precondition check reasons about the argument
+expression and the enclosing <code>if</code> guards only — it does not track
local
+assignments there, so <code>int sq = k * 1; isqrt(sq)</code> is outside scope
+(<code>sq</code> is unconstrained at the call). For a
<strong>postcondition</strong>, the body
+walker does follow each execution path through straight-line code,
+<code>if</code>/<code>else</code> and single-assignment locals. Either way the
edges of the
+fragment — loops, re-assignment, method calls, division, arrays,
+quantifiers — are reported as skipped, loudly, rather than waved
+through. That is the same trade made throughout this post:
+flow-sensitive work lives outside the type system, declarations carry
+the contract, and the type stays simple while the checker does the work.</p>
</div>
<div class="paragraph">
<p>One engineering detail is worth surfacing because it reframes what a
@@ -1283,15 +1321,13 @@ perfectly fine thing for it to do.</p>
<h3 id="_where_it_could_go">Where it could go</h3>
<div class="paragraph">
<p>The scaffold generalises along the lines OpenJML’s taxonomy suggests,
-each a new obligation site on the same solver pipeline: array-bounds
-and division-by-zero as <strong>implicit</strong> preconditions (<code>0
⇐ i && i <
+each a new obligation site on the same solver pipeline. Postconditions
+already work (above); the natural next steps are array-bounds and
+division-by-zero as <strong>implicit</strong> preconditions (<code>0 ⇐ i
&& i <
arr.size()</code>, <code>divisor != 0</code>) fired automatically at each
index or
-division; then <code>@Ensures</code> postconditions, which need symbolic
-execution of the body — the jump from per-call to per-method
-reasoning; then <code>@Invariant</code>/<code>@Decreases</code> as the
classical inductive
-loop proof. Each is strictly smaller than a GEP, and none needs a
-compiler change. The spike deliberately ships one check done well
-rather than five done shakily.</p>
+division, and then <code>@Invariant</code>/<code>@Decreases</code> as the
classical
+inductive loop proof. Each is strictly smaller than a GEP, and none
+needs a compiler change.</p>
</div>
</div>
<div class="sect2">
@@ -1304,16 +1340,18 @@ rather than five done shakily.</p>
<ul>
<li>
<p><a
href="https://github.com/paulk-asert/groovy6-functional/tree/main/verification";><code>verification/</code></a>
-— a sibling <code>@Requires</code> annotation and its text-capturing
transformation,
-the path-condition collector, the Groovy-to-SMT encoder, the
-<code>VerifyChecker</code> type-checking extension, and the Z3 backend.
+— sibling <code>@Requires</code>/<code>@Ensures</code> annotations and their
text-capturing
+transformations, the path-condition collector and body-path walker,
+the Groovy-to-SMT encoder, the <code>VerifyChecker</code> type-checking
extension,
+and the Z3 backend.
Tweaking Groovy’s existing <code>@Requires</code> wasn’t pursued
here but would be a natural next step if taking this further.</p>
</li>
<li>
<p><a
href="https://github.com/paulk-asert/groovy6-functional/tree/main/verification-demo";><code>verification-demo/</code></a>
— the <code>ISqrt</code> producer, a <code>GoodCalls</code> consumer that
compiles only
-because every call is proven safe, and a <code>BadCalls</code> runner that
-prints the diagnostics for the wrong calls.</p>
+because every call is proven safe, a <code>BadCalls</code> runner that prints
the
+diagnostics for the wrong calls, and
<code>MinMax</code>/<code>BadEnsures</code> doing the
+same for <code>@Ensures</code> postconditions.</p>
</li>
</ul>
</div>
@@ -1586,10 +1624,11 @@ builder and builder-with-checker variants, and the
<code>verification</code>
<div class="paragraph">
<p><strong>30/May/2026</strong>: Added "From contract-grade to proof-grade"
section — a
spike that puts a Z3 solver behind a <code>@TypeChecked</code> extension to
-discharge <code>@Requires</code> preconditions at compile time, with
Dafny-style
-counterexamples, for a linear-integer fragment. Notes that Groovy’s
-contract annotations echo Dafny’s keywords and OpenJML’s taxonomy.
-Two new companion subprojects, <code>verification</code> and
<code>verification-demo</code>.</p>
+discharge <code>@Requires</code> preconditions and <code>@Ensures</code>
postconditions at
+compile time, with Dafny-style counterexamples, for a linear-integer
+fragment. Notes that Groovy’s contract annotations echo Dafny’s
+keywords and OpenJML’s taxonomy. Two new companion subprojects,
+<code>verification</code> and <code>verification-demo</code>.</p>
</div>
<div class="paragraph">
<p><strong>26/May/2026</strong>: Added "Building your own checked DSL" section
diff --git a/search/search-index.json b/search/search-index.json
index b051062..81e8379 100644
--- a/search/search-index.json
+++ b/search/search-index.json
@@ -240,7 +240,7 @@
{
"id": "blog/groovy6-functional.html",
"title": "The Apache Groovy programming language - Blogs - Groovy 6
features for Functional Programmers",
- "content": "The Apache Groovy programming language - Blogs - Groovy 6
features for Functional Programmers Socialize Discuss on the mailing list
Groovy on X Groovy on Bluesky Groovy on Mastodon Groovy on LinkedIn Events and
conferences Source code on GitHub Report issues in Jira Stack Overflow
questions Slack Community You are using an outdated browser. Please upgrade
your browser to improve your experience. Apache Groovy™ Learn
Documentation Download Support Contribute Ecos [...]
+ "content": "The Apache Groovy programming language - Blogs - Groovy 6
features for Functional Programmers Socialize Discuss on the mailing list
Groovy on X Groovy on Bluesky Groovy on Mastodon Groovy on LinkedIn Events and
conferences Source code on GitHub Report issues in Jira Stack Overflow
questions Slack Community You are using an outdated browser. Please upgrade
your browser to improve your experience. Apache Groovy™ Learn
Documentation Download Support Contribute Ecos [...]
"url": "blog/groovy6-functional.html",
"site": "dev"
},
