INVSC

"Your code is only as good as your invariants."

The Invariant Scala Compiler is a “compiler” for the Scala programming language, designed to be used in the Imperative Programming course in The University of Oxford.

INVSC parses your commented code and judges it like an Oxford tutor, checking that every loop in your Scala code has properly annotated invariants and variants, and determining whether your comments are adequate to prove correctness for your program. INVSC grades your code using the "Oxford scoring system", and refuses to compile anything below α-β.

Disclaimer

This project was created as a submission for a Hackathon hosted by the Oxford Computing and Technology Society. The theme of the Hackathon was "Convoluted".

In order to evaluate your code and comments, we send your code to ChatGPT using a provided OpenAI access token. By using this software, you acknowledge that your code will be trasmitted to OpenAI's servers for processing and may be used for training future LLM models in accordance OpenAI's Terms and Conditions. You further acknowledge that we accept no responsibility for how OpenAI processes, stores, or uses your data.

Before using this software, make sure that you have set usage limits for your OpenAI access token and have reviewed and validated the contents of gpt_client.py. We do not guarantee or assume responsibility for token usage and accept no liability for any costs or expenses incurred.

Grading System

Grade	Meaning	Result
α (Alpha)	First Class Honours	✅ Compiles with fanfare
αβ (Alpha-Beta)	Upper Second	✅ Compiles with mild approval
β (Beta)	Lower Second	❌ Compilation DENIED
γ (Gamma)	Third Class	❌ Compilation VIOLENTLY DENIED

Prerequisites

• Scala
• Java JDK

Installation

# Set your OpenAI API key
export OPENAI_API_KEY="sk-..."

# Install INVSC
pip install -e .

You also need scalac on your PATH for actual compilation:

# macOS
brew install scala

# Or via Coursier (recommended)
cs install scala

Usage

# Basic usage — check invariants and compile with scalac
invsc Main.scala

# Just check invariants, don't compile
invsc --no-compile Sort.scala

# Get raw JSON output
invsc --json Search.scala

# Force compile despite shameful grade (not recommended)
invsc --force Spaghetti.scala

# Skip the dramatic grade actions
invsc --no-action Main.scala

# Use a specific model
invsc --model gpt-4o-mini Main.scala

What INVSC Checks

For every loop in your Scala code, INVSC verifies:

1. Invariant annotation — Does the loop have a comment specifying its invariant?
2. Variant annotation — Does the loop have a comment specifying its variant (termination measure)?
3. Correctness — Are the stated invariants actually correct?
4. Variant decrease — Does the variant actually decrease on each iteration?

Grade Actions

• Alpha: Triumphant announcement via macOS say
• Alpha-Beta: Mild acknowledgement
• Beta: Strongly worded letter to your Director of Studies
• Gamma: Threatens to delete your code (doesn't actually)

Example

object Sum {
  def sum(arr: Array[Int]): Int = {
    var s = 0
    var i = 0
    // Invariant: s == sum of arr(0..i-1)
    // Variant: arr.length - i
    while (i < arr.length) {
      s += arr(i)
      i += 1
    }
    s
  }
}

License

MIT