Show counterexample values in the final expected refinement
Ninguém assumiu esta issue ainda.
Avaliação
- Dificuldade
- 4/5
- Tempo estimado
- 3-5 dias
- Facilidade para iniciantes
- 55/100
Direção de pesquisa
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.
Escrita pelo modelo de indexação a partir do texto da issue.
Descrição
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.
- Linguagem predominante
- Java
- Estrelas
- 67
- Forks
- 36
- Merge médio
- 7d 48min
- PRs com merge (30d)
- 2
Preparar o ambiente
Primeiros passos
- Leia a issue inteira e depois o guia de contribuição do projeto.
- Comente na issue dizendo que vai assumir — evita que duas pessoas façam o mesmo trabalho.
- Faça um fork do repositório e trabalhe em uma branch.
- Abra um pull request que referencie o número da issue.
Mais de liquid-java/liquidjava
-
enhancement error messages future ide
Dificuldade 5/5 Mais de uma semana Facilidade para iniciantes 35/100
liquid-java/liquidjava#298 ·
-
Dificuldade 4/5 3-5 dias Facilidade para iniciantes 48/100
liquid-java/liquidjava#297 ·
-
Dificuldade 4/5 3-5 dias Facilidade para iniciantes 48/100
liquid-java/liquidjava#295 ·
-
Add a flag -a to show all verification conditions sent to the smt solverTalvez livre de novo @CatarinaGamboa assumiu há 117 dias e não há nenhum pull request aberto. Abertaenhancement
liquid-java/liquidjava#240 · 1 responsável ·
-
enhancement ide
Dificuldade 3/5 1-2 dias Facilidade para iniciantes 45/100
liquid-java/liquidjava#206 ·
Todas as issues de liquid-java/liquidjava
Issues semelhantes
-
P2 testing
Dificuldade 1/5 Menos de uma hora Facilidade para iniciantes 90/100
Mantenedores costumam responder em até 1 dia
-
area/core kind/bug status/triage team/core-shared
Dificuldade 2/5 1-3 horas Facilidade para iniciantes 82/100
Mantenedores costumam responder em até 1 dia
-
Dificuldade 2/5 1-3 horas Facilidade para iniciantes 88/100
checkstyle/checkstyle#21755 · 1 comentário ·
Mantenedores costumam responder em até 1 dia
-
Dificuldade 2/5 1-3 horas Facilidade para iniciantes 78/100
spring-projects/spring-integration#11495 ·
Mantenedores costumam responder em até 2 dias
-
Dificuldade 2/5 1-3 horas Facilidade para iniciantes 84/100
Mantenedores costumam responder em até 1 dia