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 b812727 2026/05/31 06:43:03: Generated dev website from
groovy-website@2a7de03
b812727 is described below
commit b812727f37cc95a0af67216c9978fc735c8f56d3
Author: jenkins <[email protected]>
AuthorDate: Sun May 31 06:43:03 2026 +0000
2026/05/31 06:43:03: Generated dev website from groovy-website@2a7de03
---
blog/groovy6-functional.html | 103 +++++++++++++++++++++++++++++++------------
search/search-index.json | 2 +-
2 files changed, 75 insertions(+), 30 deletions(-)
diff --git a/blog/groovy6-functional.html b/blog/groovy6-functional.html
index 03f265a..075dc52 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_and_postcondition_checker">From
contract-grade to proof-grade: an SMT-backed precondition and postcondition
checker</h2>
+<h2
id="_from_contract_grade_to_proof_grade_an_smt_backed_precondition_postcondition_and_loop_checker">From
contract-grade to proof-grade: an SMT-backed precondition, postcondition, and
loop checker</h2>
<div class="sectionbody">
<div class="paragraph">
<p>The previous demo wrote a <strong>structural</strong> checker — names,
arity, field
@@ -1134,8 +1134,9 @@ 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 covers two of
-those checks (preconditions and postconditions) over one fragment
+solver behind a type-checking extension. The spike below covers
+preconditions, postconditions, and loops (<code>@Invariant</code> plus a
+<code>@Decreases</code> termination measure) 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>
@@ -1195,10 +1196,9 @@ the model is the counterexample:</p>
</div>
<div class="paragraph">
<p>That last line is the whole point. The diagnostic does not say
-"constraint not satisfied"; it says <strong>with <code>n = -1</code> it
fails</strong>, the way
-Dafny does — and here it is the default, not a <code>--counterexample</code>
-flag. Tighten the guard and the obligation discharges; the same code
-now compiles clean:</p>
+"constraint not satisfied"; it says <strong>with <code>n = -1</code> it
fails</strong>, as Dafny
+does if you ask it (via <code>--counterexample</code>). Tighten the guard and
the
+obligation discharges; the same code now compiles clean:</p>
</div>
<div class="listingblock">
<div class="content">
@@ -1293,25 +1293,68 @@ examples.</p>
</div>
</div>
<div class="sect2">
+<h3 id="_loops_too">Loops, too</h3>
+<div class="paragraph">
+<p>Loops are the classical inductive case, and the same solver handles them
+straight from the <strong>stock</strong>
<code>@groovy.contracts.Invariant</code>/<code>@Decreases</code>
+that groovy-contracts already runtime-checks. Each annotated <code>while</code>
+raises four obligations (establishment,
+preservation, use, and — from <code>@Decreases</code> — termination), and a
broken
+one is named, with a counterexample:</p>
+</div>
+<div class="listingblock">
+<div class="content">
+<pre class="prettyprint highlight"><code data-lang="groovy">@Requires({ n
>= 0 })
+@Ensures({ result == n })
+static int countUp(int n) {
+ int i = 0
+ @Invariant({ 0 <= i && i <= n })
+ @Decreases({ n - i })
+ while (i < n) {
+ i = i + 2 // overshoots n — the invariant is not preserved
+ }
+ return i
+}</code></pre>
+</div>
+</div>
+<div class="listingblock">
+<div class="content">
+<pre class="prettyprint highlight"><code>[Static type checking] - Cannot prove
loop invariant is preserved by the loop body in countUp
+ invariant: ((0 <= i) && (i <= n))
+ counterexample: i = 0, n = 1</code></pre>
+</div>
+</div>
+<div class="paragraph">
+<p>Restore <code>i = i + 1</code> and all four obligations discharge; weaken
the
+invariant or break the measure and the diagnostic points at exactly
+which one fails. Because the annotations are the stock ones, the same
+loop also keeps its groovy-contracts runtime check — proof-grade at
+compile time, contract-grade at run time, from one declaration. The
+companion repo’s <code>Loops</code>/<code>BadLoops</code> carry one
mutant per obligation.</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, and the scope differs by mode. At a
+<p>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:
+walker follows each execution path through straight-line code,
+<code>if</code>/<code>else</code> and single-assignment locals; a
<code>while</code> carrying an
+<code>@Invariant</code> is discharged inductively (its body may re-assign). The
+remaining edges of the fragment — un-annotated loops, method calls,
+division, arrays, quantifiers, non-linear arithmetic — 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
-type-checking extension <strong>is</strong>. This extension does not merely
reference
-Z3 — it <strong>runs</strong> Z3 while the consumer compiles. A type-checking
+<p>One engineering detail reframes what a type-checking extension
<strong>is</strong>:
+this extension does not merely reference Z3 — it <strong>runs</strong> Z3
while the
+consumer compiles. A type-checking
extension is just code on the compiler’s classpath, free to call out
to anything on the JVM; "runs a theorem prover during `groovyc`" is a
perfectly fine thing for it to do.</p>
@@ -1322,12 +1365,12 @@ perfectly fine thing for it to do.</p>
<div class="paragraph">
<p>The scaffold generalises along the lines OpenJML’s taxonomy suggests,
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 <
+and loops 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, 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>
+division, and then bounded quantifiers for sortedness and
+"every element satisfies P" facts. Each is strictly smaller than a GEP,
+and none needs a compiler change.</p>
</div>
</div>
<div class="sect2">
@@ -1340,18 +1383,20 @@ needs a compiler change.</p>
<ul>
<li>
<p><a
href="https://github.com/paulk-asert/groovy6-functional/tree/main/verification";><code>verification/</code></a>
-— 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>
+— a <code>CONVERSION</code>-phase transform that captures each stock
+<code>@groovy.contracts</code> contract’s source text into a
<code>@ContractSource</code> the
+checker can read back (the built-in annotation keeps only a generated
+closure class, so the text would otherwise be gone), the path-condition
+collector, the body-path walker and loop verifier, the Groovy-to-SMT
+encoder, the <code>VerifyChecker</code> type-checking extension, and the Z3
backend.</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, 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>
+diagnostics for the wrong calls, <code>MinMax</code>/<code>BadEnsures</code>
doing the same
+for <code>@Ensures</code> postconditions, and
<code>Loops</code>/<code>BadLoops</code> for
+<code>@Invariant</code>/<code>@Decreases</code> loop proofs.</p>
</li>
</ul>
</div>
diff --git a/search/search-index.json b/search/search-index.json
index 81e8379..1d2dda1 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"
},
