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 55dbb58 openjml inspired example (also loop invariants)
55dbb58 is described below
commit 55dbb5814350d51fcf27e3fe48eca9e258e440f5
Author: Paul King <[email protected]>
AuthorDate: Sun May 31 18:01:18 2026 +1000
openjml inspired example (also loop invariants)
---
site/src/site/blog/groovy6-functional.adoc | 11 ++++++-----
1 file changed, 6 insertions(+), 5 deletions(-)
diff --git a/site/src/site/blog/groovy6-functional.adoc
b/site/src/site/blog/groovy6-functional.adoc
index 9bad5e3..fd98d12 100644
--- a/site/src/site/blog/groovy6-functional.adoc
+++ b/site/src/site/blog/groovy6-functional.adoc
@@ -1267,11 +1267,12 @@ builder and builder-with-checker variants, and the
`verification`
****
*30/May/2026*: Added "From contract-grade to proof-grade" section — a
spike that puts a Z3 solver behind a `@TypeChecked` extension to
-discharge `@Requires` preconditions and `@Ensures` 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,
-`verification` and `verification-demo`.
+discharge `@Requires` preconditions, `@Ensures` postconditions, and
+`@Invariant`/`@Decreases` loops at compile time, with Dafny-style
+counterexamples, for a linear-integer fragment. It reads Groovy's
+built-in `@groovy.contracts` annotations directly, and notes how their
+names echo Dafny's keywords and OpenJML's taxonomy. Two new companion
+subprojects, `verification` and `verification-demo`.
*26/May/2026*: Added "Building your own checked DSL" section
demonstrating the producer/consumer split transferred to library
