Show counterexample values in the final expected refinement
Nessuno ha ancora preso questa issue.
Valutazione
- Difficoltà
- 4/5
- Tempo stimato
- 3-5 giorni
- Idoneità per principianti
- 55/100
Direzione di ricerca
Start at the refinement-error diagnostic and trace the final expected predicate used for verification through alias and state expansion and simplification. Add tests covering multiple assignments, repeated variables, aliases, and values that cannot be represented safely. Done means the original refinement and assignments remain, while the final predicate shows substituted values without reducing the informative expression.
Scritto dal modello di indicizzazione a partire dal testo della issue.
Descrizione
A refinement error currently shows the original expected refinement and counterexample assignments separately. Include a readable version of the final expected predicate used for verification, after alias and state expansion and any applicable simplification, with every available counterexample value substituted.
For example:
Original expected: Positive(buffered)
Final expected: buffered > 0
Counterexample: buffered == 0
With witness: 0 > 0 ✗
Substitute using expression variable identities, without hardcoded alias names or text replacement. Keep the informative expression (0 > 0) rather than reducing it to false. Preserve the original expected refinement and assignments; leave values unchanged when they cannot be represented safely. Cover multiple assignments, repeated variables, and aliases in tests.
Related to #295, which covers navigating alias expansion in the diagnostic history.
- Lingua principale
- Java
- Stelle
- 67
- Fork
- 36
- Merge medio
- 7g 48m
- PR unite (30g)
- 2
Preparare l'ambiente
Come iniziare
- Leggi tutta la issue e poi la guida ai contributi del progetto.
- Commenta sulla issue per dire che te ne occupi tu — evita che due persone facciano lo stesso lavoro.
- Fai un fork del repository e lavora su un branch.
- Apri una pull request che faccia riferimento al numero della issue.
Altre issue di liquid-java/liquidjava
-
enhancement error messages future ide
Difficoltà 5/5 Più di una settimana Idoneità per principianti 35/100
liquid-java/liquidjava#298 ·
-
Difficoltà 4/5 3-5 giorni Idoneità per principianti 48/100
liquid-java/liquidjava#297 ·
-
Difficoltà 4/5 3-5 giorni Idoneità per principianti 48/100
liquid-java/liquidjava#295 ·
-
Add a flag -a to show all verification conditions sent to the smt solverForse di nuovo libera @CatarinaGamboa l’ha presa 118 giorni fa e non c’è nessuna pull request aperta. Apertaenhancement
liquid-java/liquidjava#240 · 1 assegnatario ·
-
enhancement ide
Difficoltà 3/5 1-2 giorni Idoneità per principianti 45/100
liquid-java/liquidjava#206 ·
Tutte le issue di liquid-java/liquidjava
Issue simili
-
bug
Difficoltà 2/5 1-3 ore Idoneità per principianti 78/100
-
component/zeebe kind/bug
Difficoltà 1/5 Meno di un'ora Idoneità per principianti 90/100
I maintainer di solito rispondono entro 1 giorno
-
Difficoltà 2/5 1-3 ore Idoneità per principianti 78/100
UniversalMediaServer/UniversalMediaServer#6356 ·
I maintainer di solito rispondono entro 1 giorno
-
Difficoltà 2/5 1-3 ore Idoneità per principianti 88/100
refinedmods/refinedstorage2#1414 · 1 commento ·
-
Difficoltà 1/5 1-3 ore Idoneità per principianti 88/100
yegor256/rultor-image#76 · 1 commento ·