Summary

A spec predicate cannot mention null: bindaddr == null ? ... : ... gives Not Found Error: Variable 'null' could not be found. So a spec cannot say what the JDK does when a parameter is null, even where that is the documented way to choose a state.

Minimal reproducer

DatagramSocketRefinements.java:

import java.net.SocketAddress;
import liquidjava.specification.*;

@ExternalRefinementsFor("java.net.DatagramSocket")
@StateSet({"unbound", "bound"})
public interface DatagramSocketRefinements {
    @StateRefinement(to = "bindaddr == null ? unbound(this) : bound(this)")
    void DatagramSocket(SocketAddress bindaddr);

    @StateRefinement(from = "unbound(this)", to = "bound(this)")
    void bind(SocketAddress addr);
}

Client.java:

import java.net.DatagramSocket;
import java.net.InetSocketAddress;

public class Client {
    public static void main(String[] args) throws Exception {
        DatagramSocket s = new DatagramSocket(null);   // Variable 'null' could not be found
        s.setReuseAddress(true);
        s.bind(new InetSocketAddress(0));
        s.close();
    }
}

Expected: Correct! Passed Verification. On the JVM this runs: DatagramSocket(SocketAddress) says "if the address is null, creates an unbound socket", so that options such as setReuseAddress can be set before binding.

Seen on 1a506fe, f7f366c and main at 19991d3.

Why it matters: real code

Without null in predicates the spec has to pick one state for the constructor. Choosing bound (what every other constructor does) rejects the documented idiom above, which real UDP code uses. Two of five mined GitHub methods using DatagramSocket do exactly this: create with null, then bind(new InetSocketAddress(IP, port)) (e.g. Padawan-Transport-Protocol-PTP Sender.createSocket). Choosing unbound instead lets bind on an already-bound socket through, which throws SocketException on the JVM.

Found while checking mined client code against JDK specs (liquid-java/co-specification, verifier probe V34).