GV

GeezerVison

The World Wide Web, restored to 800 pixels of glory.

Home|About|Gaming cabinet|Archives|How it works|Starter sites

On this site

  • Sign in
  • ActionsCI/CD and automation
  • CodespacesCloud development environments
  • All Features
  • Documentation
  • Training
  • Certifications
  • Build with Copilot
  • Customize Copilot
  • Integrations
  • Trending repos
  • GitHub Sponsors
  • Developer articles
  • Enterprises

This view

  • Original page
  • New address

GeezerVison is showing github.com — GitHub - liquid-java/liquidjava-examples: Code examples demonstrating LiquidJava refinement types and typestate verification

BranchesTags
Open more actions menu

Latest commit

 

History

100 Commits
100 Commits

Folders and files

NameName
Last commit message
Last commit date
.devcontainer
.devcontainer
 
 
examples/demo
examples/demo
 
 
figs
figs
 
 
user_study_23
user_study_23
 
 
.gitignore
.gitignore
 
 
README.md
README.md
 
 

Repository files navigation

LiquidJava Examples

Welcome to the LiquidJava examples repository!

This collection demonstrates how to use LiquidJava, a powerful extension for Java that enables expressive type refinements through annotations. Whether you're new to LiquidJava or looking to deepen your understanding, these examples will help you explore its capabilities and learn how to enhance your Java code with sophisticated type checking.

For more information about LiquidJava, visit our website!

Setup Instructions

Using Codespaces

  • To use Codespaces, make sure you’re logged in to GitHub, click the button below, select 4-core, and then press Create codespace. The codespace will open in your browser and with the LiquidJava extension installed.

    Open in GitHub Codespaces

Using Dev Containers

  • You can also use VS Code's Dev Containers. Make sure you have Docker and the Dev Containers extension installed in VS Code and use the "Remote-Containers: Open Folder in Container" command.

Local Setup

  • Alternatively, you can use the extension locally in your VS Code, by pulling this repository and installing the extension from the marketplace, which is available here.
  • Ensure the Red Hat extension for Language Support for Java™ is also installed and enabled.
  • Make sure to have at least Java 20+ and Maven 3.6+ installed on your machine.
  • Execute the following commands in your terminal:
git clone https://github.com/CatarinaGamboa/liquidjava-examples
cd liquidjava-examples/examples/demo
mvn clean install

Using the Extension

  1. When opening a Java project, the extension will automatically verify your LiquidJava annotations.
  2. Errors will be reported in real-time and refinements will have syntax highlighting.
  3. An item in the status bar at the bottom left of the editor indicates the extension's current state. You can check the extension logs by clicking on it.

Examples

liquidjava-examples/
├── examples/                          
│   ├── demo/                           # Simple demo examples
│   │   ├── src/main/java/com/example   # Examples start with "Test*.java"
├── user_study_23/                      # Example projects used for user study of 2023
│   ├── part1-plainJava/                # Java projects without LiquidJava
│   ├── part3-liquidJava/               # Projects with LiquidJava annotations
│   └── part4/                          # Files to be annotated with LiquidJava
├── extension/                          # Contains the VSIX extension file
...

2022/23 User Study:

part1-plainJava

Contains Java projects without LiquidJava. Open one of the folders on VS Code and find the error.

part3-liquidJava

Contains LiquidJava projects.

Open one of the folders on VS Code with the extension running. Uncomment the code in the Test file and find the error. You can open the folder through the terminal by going to the correct path and typing code or open through the VS Code GUI.

part4

Contains Java files to be annotated with LiquidJava.

  • Variable.java - Add the annotation and check the correct and wrong assignment
  • TrafficLight.java - Add the annotations on the fields and model the state using @StateSet and @StateRefinement. To check if the modelling is correct, uncomment the file TestTLCorrect.java (that should be correct) and then uncomment the file TestTLWrong.java that should present an error.

Advanced Development

For extension development:

  • Refer to the VS Code Extension API documentation
  • Make changes to your code and test using the provided examples
  • Use the debug console to troubleshoot any issues

About

Code examples demonstrating LiquidJava refinement types and typestate verification

liquid-java.github.io/

Topics

code-samplesexamplesjava-examplesliquid-typesrefinement-typesstatic-verificationtutorial

Resources

Readme
Activity
Custom properties

Stars

5 stars

Watchers

3 watching

Forks

2 forks
Report repository

Releases

Packages

Used by

Contributors

Languages

You are visitor 01402503 — GeezerVison does not store the pages you look up.
Best viewed with Netscape Navigator 4.7 or Internet Explorer 6 at 800×600. No cookies required.