You are viewing a plain text version of this content. The canonical link for it is here.
Posted to commits@groovy.apache.org by gi...@apache.org on 2026/07/04 03:19:08 UTC
(groovy-dev-site) branch asf-site updated: 2026/07/04 03:19:03: Generated dev website from groovy-website@95ad847
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 315f9f34 2026/07/04 03:19:03: Generated dev website from groovy-website@95ad847
315f9f34 is described below
commit 315f9f341ed9bedec468b84b282186453a286137
Author: jenkins <bu...@apache.org>
AuthorDate: Sat Jul 4 03:19:03 2026 +0000
2026/07/04 03:19:03: Generated dev website from groovy-website@95ad847
---
blog/feed.atom | 11 ++++++
blog/groovy6-formal-methods.html | 79 ++++++++++++++++++++++++++++++++++------
blog/index.html | 4 +-
search/search-index.json | 4 +-
4 files changed, 83 insertions(+), 15 deletions(-)
diff --git a/blog/feed.atom b/blog/feed.atom
index ef14c5c3..7b7b737e 100644
--- a/blog/feed.atom
+++ b/blog/feed.atom
@@ -16,6 +16,17 @@
<published>2026-07-01T11:00:00Z</published>
<summary type="html">Reproduce a viral astronomy demo in groovysh: load galaxy images and spectra from Hugging Face's Multimodal Universe and render them inline with /img.</summary>
</entry>
+ <entry>
+ <id>http://groovy.apache.org/blog/groovy6-formal-methods</id>
+ <author>
+ <name>Paul King</name>
+ </author>
+ <title type="html">Groovy 6 features for formal method advocates</title>
+ <link href="http://groovy.apache.org/blog/groovy6-formal-methods"/>
+ <updated>2026-06-25T08:00:00Z</updated>
+ <published>2026-06-25T08:00:00Z</published>
+ <summary type="html">Groovy 6 ships design-by-contract &amp; type-checking extensions. The groovy-verify project turns those contracts into Dafny-style proofs with counterexamples.</summary>
+ </entry>
<entry>
<id>http://groovy.apache.org/blog/fizzbuzz-with-groovy-and-emojis</id>
<author>
diff --git a/blog/groovy6-formal-methods.html b/blog/groovy6-formal-methods.html
index b6eb740e..17b62d1c 100644
--- a/blog/groovy6-formal-methods.html
+++ b/blog/groovy6-formal-methods.html
@@ -140,10 +140,8 @@ humans and agents</a>.</p>
</div>
<div class="paragraph">
<p>A note on versions before we start: <code>groovy-verify</code> tracks Groovy 6
-closely, and the recommended pairing right now is <strong>Groovy 6.0.0-alpha-2</strong>,
-currently out for an Apache release vote with staged artifacts in the
-<a href="https://repository.apache.org/content/repositories/orgapachegroovy-1109">ASF
-staging repository</a>. Everything below was written against that pairing.</p>
+closely, and the recommended pairing is <strong>Groovy 6.0.0-alpha-2</strong> or later.
+Everything below was written against that pairing.</p>
</div>
</div>
</div>
@@ -941,6 +939,47 @@ that demands a minimum balance is refuted, with the input that breaks
substitutability.</p>
</div>
<div class="paragraph">
+<p><strong>Even (some) dynamic Groovy.</strong> Everything above lives in Groovy’s statically
+checkable subset — <code>@TypeChecked</code> is the front door, so runtime
+metaprogramming has been out of scope by construction. But Groovy’s type
+checking is extensible in <em>two directions</em>: an extension can <strong>strengthen</strong>
+checking (groovy-verify itself is exactly that), and it can <strong>selectively
+relax</strong> it — type what looks like uncheckable dynamic code when there is
+evidence to type it from. The experimental metaprogramming pack does both at
+once: when an <code>ExpandoMetaClass</code> registration is spelled out in the same
+class, it types the registration and its use sites under <code>@TypeChecked</code>, then
+inlines the registered closure into the proof. The metaclass FizzBuzz examples
+from
+<a href="https://groovy.apache.org/blog/fizzbuzz-with-groovy-and-emojis">FizzBuzz with
+Groovy and emojis</a> verify against exact specifications this way:</p>
+</div>
+<div class="listingblock">
+<div class="content">
+<pre class="prettyprint highlight"><code data-lang="groovy">static {
+ Integer.metaClass.multiply = { String s -> delegate == 0 ? s : '' }
+}
+@Ensures({ result == (n % 3 == 0 && n % 5 == 0 ? '🥤🐝' : n % 3 == 0 ? '🥤' : n % 5 == 0 ? '🐝' : '') })
+static String emoji(int n) { (n % 3) * '🥤' + (n % 5) * '🐝' } // VERIFIED</code></pre>
+</div>
+</div>
+<div class="paragraph">
+<p>The gate is deliberately narrow and evidence-backed: no visible registration,
+no blessing — the code stays a compile error, exactly as <code>@TypeChecked</code>
+demands.</p>
+</div>
+<div class="paragraph">
+<p><strong>Functional proofs, Verus-style.</strong> Not everything needs a loop invariant: a
+method’s own <code>@Ensures</code> is assumed at its recursive call sites (sound because
+<code>@Decreases</code> proves termination) — which is proof by induction — and a <code>void</code>
+method whose only job is to carry an <code>@Ensures</code> acts as a lemma or theorem.
+The repo’s functional leftpad proves all three of the classic challenge
+properties this way, with a <em>structural</em> specification
+(<code>result == pads(pad, n - s.length()) + s</code> — the output <strong>is</strong> the padding
+block followed by the original string) and the length property derived from a
+padding-length lemma by a theorem method — the spec-function / proof-function
+structure of Verus, done with plain Groovy methods.</p>
+</div>
+<div class="paragraph">
<p>And, more briefly, the repo also demonstrates:</p>
</div>
<div class="ulist">
@@ -969,6 +1008,22 @@ max-by-elimination, and <em>Modeling Concurrency in Dafny</em>'s ticket lock (sa
in Groovy.</p>
</li>
<li>
+<p><strong>Hillel Wayne’s <a href="https://www.hillelwayne.com/post/theorem-prover-showdown/">Theorem
+Prover Showdown</a></strong> with full specifications — leftpad (imperative <em>and</em> the
+functional-by-induction form above), unique with a bidirectional spec, and
+fulcrum’s argmin — plus mergesort’s <code>merge</code> proved sorted <em>and</em> a permutation
+across three sequential annotated loops. Two Groovy entries (imperative and
+functional) have been submitted to the community’s
+<a href="https://github.com/hwayne/lets-prove-leftpad">lets-prove-leftpad</a> collection.</p>
+</li>
+<li>
+<p><strong>Encoding packs</strong> — domain vocabularies plug in as <code>ServiceLoader</code>-discovered
+modules (packs model <em>libraries</em>, the core models the <em>language</em>): number
+theory (Fibonacci/GCD recurrences, extended with Bézout coefficients through
+which Gauss’s lemma proves), the whole JSR 385 units domain, combinatorics
+(factorials and Pascal-rule binomials), and the metaprogramming pack above.</p>
+</li>
+<li>
<p><strong>Verifying Java fragments</strong> — since Java is largely a syntactic subset of
Groovy, many integer/array algorithms verify by reading the Java source <em>as
Groovy</em> (with the honest caveat that the proof is over Groovy semantics).</p>
@@ -1083,9 +1138,7 @@ separation logic). Anything outside the fragment is reported as "skipped",
never silently passed.</p>
</li>
<li>
-<p>The recommended pairing today is <strong>Groovy 6.0.0-alpha-2</strong>, currently out for
-an Apache release vote (staged artifacts
-<a href="https://repository.apache.org/content/repositories/orgapachegroovy-1109">here</a>).</p>
+<p>The recommended pairing today is <strong>Groovy 6.0.0-alpha-2</strong> or later.</p>
</li>
</ul>
</div>
@@ -1223,13 +1276,14 @@ external <code>groovy-verify</code> project reads the <strong>same</strong> cont
<strong>same</strong> <code>@TypeChecked</code> extension SPI, proves them with Z3 — or refutes them
with the exact input that breaks them. Postconditions, bounds, null,
overflow, class invariants, loop termination, the multiset-conservation of a
-real sort, information flow, dimensional analysis, Liskov subtyping, and
-algebraic laws are all in reach for the fragment it models.</p>
+real sort, information flow, dimensional analysis, Liskov subtyping,
+algebraic laws, functional proofs by induction — and even statically-visible
+metaclass programming — are all in reach for the fragment it models.</p>
</li>
<li>
<p><strong>Honestly:</strong> <code>groovy-verify</code> is experimental and not part of Groovy; it is
loudly partial, sound within its fragment and explicit about its edges; and
-the recommended pairing is the in-vote 6.0.0-alpha-2.</p>
+the recommended pairing is 6.0.0-alpha-2 or later.</p>
</li>
<li>
<p><strong>And increasingly:</strong> because the contracts are machine-readable, the proofs
@@ -1286,12 +1340,15 @@ Design-by-Contract module shipped with Groovy</p>
<p><a href="https://groovy.apache.org/blog/groovy-null-checker">Compile-time null safety for Groovy</a> — the <code>NullChecker</code> walkthrough</p>
</li>
<li>
-<p><a href="https://repository.apache.org/content/repositories/orgapachegroovy-1109">Groovy 6.0.0-alpha-2 staged artifacts</a> (currently in the release vote)</p>
+<p><a href="https://groovy.apache.org/download.html">Groovy 6.0.0-alpha-2</a> (also on Maven Central)</p>
</li>
<li>
<p><a href="https://dafny.org">Dafny</a> and <a href="https://github.com/verus-lang/verus">Verus</a> — the auto-active verifiers whose specification style and counterexample UX this echoes</p>
</li>
<li>
+<p><a href="https://www.hillelwayne.com/post/theorem-prover-showdown/">The Theorem Prover Showdown</a> and <a href="https://github.com/hwayne/lets-prove-leftpad">lets-prove-leftpad</a> — Hillel Wayne’s challenges, answered above</p>
+</li>
+<li>
<p><a href="https://leino.science/papers/krml260.pdf">K. Rustan M. Leino, <em>Modeling Concurrency in Dafny</em> (KRML 260)</a> — the ticket-lock development (safety and liveness) reproduced above</p>
</li>
<li>
diff --git a/blog/index.html b/blog/index.html
index afca1b6e..51bb6dfa 100644
--- a/blog/index.html
+++ b/blog/index.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' id='blog-index'><ul class='nav-sidebar list'><li class='active'><a href='/blog/'>Blogs</a></li><li><a href='multimodal-universe-with-groovy'>Exploring the Multimodal Universe with Groovy™</a></li><li><a href='fizzbuzz-with-groovy-and-emojis'>FizzBuzz with Groovy and Emojis</a></li><li><a href='groovy6-functional'>Groovy 6 features for Functional Programmers</ [...]
+ </div><div id='content' class='page-1'><div class='row'><div class='row-fluid'><div class='col-lg-3' id='blog-index'><ul class='nav-sidebar list'><li class='active'><a href='/blog/'>Blogs</a></li><li><a href='multimodal-universe-with-groovy'>Exploring the Multimodal Universe with Groovy™</a></li><li><a href='groovy6-formal-methods'>Groovy 6 features for formal method advocates</a></li><li><a href='fizzbuzz-with-groovy-and-emojis'>FizzBuzz with Groovy and Emo [...]
<div class='row'>
<div class='colset-3-footer'>
<div class='col-1'>
@@ -107,7 +107,7 @@
colors: am5.ColorSet.new(root, {})
}));
wc.data.setAll([
- { category: "groovy", value: 93 }, { category: "asf", value: 2 }, { category: "apachecon", value: 3 }, { category: "communityovercode", value: 2 }, { category: "natural language processing", value: 2 }, { category: "nlp", value: 1 }, { category: "nlpcraft", value: 1 }, { category: "combinations", value: 1 }, { category: "permutations", value: 1 }, { category: "testing", value: 2 }, { category: "junit", value: 2 }, { category: "spock", value: 2 }, { category: "jqwik", valu [...]
+ { category: "groovy", value: 93 }, { category: "asf", value: 2 }, { category: "apachecon", value: 3 }, { category: "communityovercode", value: 2 }, { category: "natural language processing", value: 2 }, { category: "nlp", value: 1 }, { category: "nlpcraft", value: 1 }, { category: "combinations", value: 1 }, { category: "permutations", value: 1 }, { category: "testing", value: 2 }, { category: "junit", value: 2 }, { category: "spock", value: 2 }, { category: "jqwik", valu [...]
]);
wc.labels.template.setAll({
paddingTop: 5,
diff --git a/search/search-index.json b/search/search-index.json
index 320c9b9a..f0aab032 100644
--- a/search/search-index.json
+++ b/search/search-index.json
@@ -730,7 +730,7 @@
{
"id": "blog/index.html",
"title": "The Apache Groovy programming language - Blogs",
- "content": "The Apache Groovy programming language - Blogs 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 Ecosystem Blog posts Socialize Blogs Exploring the [...]
+ "content": "The Apache Groovy programming language - Blogs 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 Ecosystem Blog posts Socialize Blogs Exploring the [...]
"url": "blog/index.html",
"site": "dev"
},
@@ -758,7 +758,7 @@
{
"id": "blog/groovy6-formal-methods.html",
"title": "The Apache Groovy programming language - Blogs - Groovy 6 features for formal method advocates",
- "content": "The Apache Groovy programming language - Blogs - Groovy 6 features for formal method advocates 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 Eco [...]
+ "content": "The Apache Groovy programming language - Blogs - Groovy 6 features for formal method advocates 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 Eco [...]
"url": "blog/groovy6-formal-methods.html",
"site": "dev"
},