@@ -81,13 +78,118 @@
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
+
+
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. +
+
+