From 9fce50576eb11a9ee9619805bbe097a172389489 Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 16 Nov 2025 16:48:40 +0000 Subject: [PATCH 1/7] Enhance LiquidJava website with improved content and structure This commit significantly improves the website with: - Add "What is LiquidJava?" section explaining refinement types clearly - Add "See It in Action" section with side-by-side code comparison showing division by zero prevention example - Add "Why LiquidJava?" section with 5 key benefits as bullet points - Add "Get Started" section with clear call-to-action and links - Reorganize research context section to footer area - Add custom CSS for better mobile responsiveness - Improve code block styling and visual hierarchy - Enhance link styling and spacing throughout The new structure follows research project best practices, similar to LiquidHaskell, Lean, and RoSpec websites. --- assets/css/style-starter.css | 111 +++++++++++++++++++++++++++++++- index.html | 119 +++++++++++++++++++++++++++++++---- 2 files changed, 216 insertions(+), 14 deletions(-) diff --git a/assets/css/style-starter.css b/assets/css/style-starter.css index 68dbd98..00f1fc4 100644 --- a/assets/css/style-starter.css +++ b/assets/css/style-starter.css @@ -12643,4 +12643,113 @@ body:after { .blog-post-card { margin-bottom: 3rem; } -} \ No newline at end of file +} +/* LiquidJava Custom Styles */ + +/* Code comparison section - responsive adjustments */ +@media (max-width: 991px) { + .col-lg-6 > div[style*="background: #272822"] { + margin-bottom: 20px; + } +} + +/* Improve spacing for new sections */ +.content-left ul { + padding-left: 20px; +} + +.content-left ul li { + margin-bottom: 10px; +} + +/* Better link styling in paragraphs */ +.content-left p a { + color: #0066cc; + text-decoration: none; + border-bottom: 1px solid transparent; + transition: border-bottom 0.2s ease; +} + +.content-left p a:hover { + border-bottom: 1px solid #0066cc; +} + +.content-left p a b { + color: #0052a3; +} + +/* Code block improvements for mobile */ +@media (max-width: 767px) { + pre { + font-size: 12px; + overflow-x: auto; + } + + div[style*="background: #272822"] { + padding: 0.5em !important; + } +} + +/* Research context section styling */ +.w3l-about .skills-bars h4 { + margin-bottom: 20px; + color: #333; +} + +/* Ensure proper spacing between sections */ +.row + br { + display: block; +} + +/* Better visual hierarchy for headings */ +.content-left h4 { + color: #2c3e50; + margin-top: 20px; + margin-bottom: 15px; +} + +.content-left h5 { + color: #34495e; + margin-bottom: 10px; +} + +/* Small text styling */ +p.small { + font-size: 14px; + color: #666; + margin-bottom: 10px; +} + +/* Feature list styling */ +.content-left ul[style*="font-size: 16px"] { + max-width: 800px; +} + +.content-left ul[style*="font-size: 16px"] li b { + color: #2c3e50; +} + +/* Responsive improvements for main heading */ +@media (max-width: 576px) { + h3 { + font-size: 24px; + } + + h4 { + font-size: 20px; + } + + h5 { + font-size: 18px; + } +} + +/* Code example section improvements */ +.content-left .row .col-lg-6 h5 { + min-height: 30px; +} + +/* Better spacing for Get Started section */ +.content-left p + p { + margin-top: 15px; +} diff --git a/index.html b/index.html index 70b611e..afb2206 100644 --- a/index.html +++ b/index.html @@ -64,16 +64,6 @@
-
-

Project developed at - Logo - - - -

-
-


content-photo @@ -81,13 +71,75 @@

Extending Java with
Liquid Types

- Extend your Java code with Refinement Types and catch bugs earlier!
- LiquidJava implements an additional type system with Refinement Types on top of Java. - It allows developers to express better restrictions on the code and discover more bugs before executing the program. + Extend your Java code with Refinement Types and catch bugs earlier!



+ + +
+
+

What is LiquidJava?

+

+ LiquidJava extends Java's type system with refinement types—types enriched with logical predicates. + This allows you to express and verify precise properties about your code, catching bugs like null pointer exceptions, + division by zero, and array index errors at compile time rather than runtime. By adding lightweight annotations to your + Java code, LiquidJava provides an additional layer of safety without requiring you to rewrite your programs. +

+
+
+
+ + +
+
+

See It in Action

+

Here's a simple example showing how LiquidJava catches potential runtime errors at compile time:

+ +
+
+
Without LiquidJava
+

Compiles but may crash at runtime

+
+ 
int divide(int a, int b) {
+    return a / b;  // potential division by zero!
+}
+
+int result = divide(10, 0);  // Runtime error!
+
+
+ +
+
With LiquidJava
+

Verified safe at compile time

+
+ 
int divide(int a, @Refinement("b != 0") int b) {
+    return a / b;  // guaranteed safe!
+}
+
+int result = divide(10, 0);  // Compile-time error!
+
+
+
+
+
+

+ + +
+
+

Why LiquidJava?

+
    +
  • Catch null pointer exceptions before runtime: Verify that objects are non-null where needed
    • +
  • Verify array bounds automatically: Ensure array indices are always within valid ranges
    • +
  • Ensure division by non-zero values: Prevent division-by-zero errors at compile time
    • +
  • Express and check custom invariants: Define and verify application-specific properties
    • +
  • Integrate with existing Java code: Add refinements incrementally to your projects
    • +
+
+
+


@@ -137,6 +189,25 @@
GitHub Repositories:
+ + +

+
+
+

Get Started

+

+ Ready to try LiquidJava? Visit our main GitHub repository + for installation instructions and comprehensive examples. You can also follow our + interactive tutorial to learn how to use + LiquidJava's capabilities step by step. +

+

+ Install the Visual Studio Code plugin + to get started with LiquidJava in your favorite IDE. +

+
+
+
@@ -583,6 +654,28 @@
+ +
+
+
+
+
+

Research Context

+

+ LiquidJava is a research project focusing on making formal verification accessible to Java developers + through refinement types. The project has been developed at LASIGE, Faculdade de Ciências, Universidade de Lisboa, + with contributions from researchers at Carnegie Mellon University. +

+
+

Project developed at

+ LASIGE and FCUL logos +
+
+
+
+
+
+