This is an automated email from the ASF dual-hosted git repository.
paulk-asert pushed a commit to branch asf-site
in repository https://gitbox.apache.org/repos/asf/groovy-website.git
The following commit(s) were added to refs/heads/asf-site by this push:
new 2af77c0 openjml inspired example
2af77c0 is described below
commit 2af77c0fefb56779e3e7e62fb3cbceda17c4600c
Author: Paul King <[email protected]>
AuthorDate: Sat May 30 14:45:24 2026 +1000
openjml inspired example
---
site/src/site/blog/groovy6-functional.adoc | 7 ++++++-
1 file changed, 6 insertions(+), 1 deletion(-)
diff --git a/site/src/site/blog/groovy6-functional.adoc
b/site/src/site/blog/groovy6-functional.adoc
index e871114..0a99551 100644
--- a/site/src/site/blog/groovy6-functional.adoc
+++ b/site/src/site/blog/groovy6-functional.adoc
@@ -1141,7 +1141,12 @@ in-tree checkers are open to library authors: a `WIRE {
name <<
call(args) }` proc-notation macro that compiles to literal
`async { df.X = … }` Groovy 6 dataflow code, with bound-name,
existence and arity checks at expansion time, ports the
-WireCat cartesian-categories idea on the same SPI surface.
+WireCat cartesian-categories idea on the same SPI surface. The
+same surface reaches further still — a type-checking extension
+that runs an SMT solver during compilation turns a contract-grade
+`@Requires` proof-grade for a linear-integer fragment, emitting
+Dafny-style counterexamples: a theorem prover hosted in `groovyc`,
+no compiler change required.
For new code on the JVM, the takeaway is that `@Pure`, `@Modifies`,
`@Associative` and `@Reducer` cover most of what teams used
