Counterexample: a guard stored in a boolean (boolean bad = a || b || c; if (bad) return;) is not split, so every variable of the guard is listed

オープン
  • 何か問題がありますか？
#471 コメント 0 件 リアクション 0 件 担当者 0 名 GitHub で見る

メンテナーはふだん 2 日以内に返信

まだ誰も着手していません。

評価

難易度
4/5
見積もり時間
3〜5日
初心者へのやさしさ
52/100
issue の種類
バグ
明瞭さ
明確に書かれている
活発さ
活発
技術スタック
java
領域
compilers

調査の方向性

Start by reading RefinementError.factsOf and how boolean definitions and negated facts are handled; the issue identifies linkedTerms and isKnown as relevant. Run the supplied Java reproducer and compare its counterexample with the expected timeout == -1. Done when the stored-boolean guard produces the expected minimal counterexample without unrelated guard variables or the generated name.

索引モデルが issue の本文から書いたものです。

説明

bug error messages

Impact: when a guard is stored in a boolean before the if, the counterexample lists values for every variable of the guard and for a generated name, instead of only the value that breaks the call. Seen on the branch of #460 (pending merge), which fixes this for an inline guard; on main the counterexample for this input has the same noise and also leaves out timeout (#453).

Minimal reproducer

import liquidjava.specification.Refinement;

public class Probe {
    static void connect(@Refinement("_ >= 0") int timeout) {}

    static void probe(int port, int retries, int timeout) {
        boolean bad = port < 0 || retries < 0 || timeout > 60000;
        if (bad) return;
        connect(timeout);
    }
}

Expected: Counterexample: timeout == -1, as with the inline guard if (port < 0 || retries < 0 || timeout > 60000) return;, which on #460's branch (712759fe) gives:

Refinement Error: !(port < 0 || retries < 0 || timeout > 60000) is not a subtype of timeout >= 0
 --> Counterexample: timeout == -1

Actual (#460's branch @ 712759fe):

Refinement Error: #fresh⁹ == (port < 0 || retries < 0 || timeout > 60000) && !#fresh⁹ is not a subtype of timeout >= 0
 7 |         boolean bad = port < 0 || retries < 0 || timeout > 60000;
 8 |         if (bad) return;
 9 |         connect(timeout);
   |         ^^^^^^^^^^^^^^^^^
10 |     }
11 | }
 --> Counterexample: timeout == -1 && port == 0 && retries == 0 && #fresh⁹ == false

main @ 0053074e prints the same Found with Counterexample: port == 0 && retries == 0 && #fresh⁹ == false.

Cause. On #460's branch, RefinementError.factsOf splits !(a || b) into !a and !b, but here found is #fresh == (a || b || c) && !#fresh. The definition is one fact that shares terms with everything, so linkedTerms pulls in port, retries and #fresh. isKnown only recognises x == v facts, so !#fresh does not hide #fresh == false. Substituting a boolean defined as x == e into !x (giving !e) before splitting would give the same facts as the inline guard. Separately, found names the local bad as #fresh⁹.

🤖 Generated with Claude Code

主要言語
Java
スター
71
フォーク
37
平均マージ
1日 19時間
マージ済み PR（30日）
46

環境構築

はじめの一歩

  1. issue を最後まで読み、次にプロジェクトのコントリビューションガイドを読みます。
  2. 着手することを issue にコメントします — 二人が同じ作業をするのを防げます。
  3. リポジトリをフォークし、ブランチを切って変更します。
  4. issue 番号を参照したプルリクエストを送ります。

liquid-java/liquidjava のほかの issue

liquid-java/liquidjava の issue をすべて見る

似ている issue

Java の issue をもっと見る

新しい issue をメールで受け取る

初心者向けの GitHub issue を短くまとめたダイジェスト。