Name

Last commit message

Last commit date

139 Commits

bootclasspath

src/main/java

.gitignore

JMEGraph_getHooks.csv

JMEGraph_getIncidentArcsFromNode.csv

JMEGraph_inv_accessible.csv

JMERuleError_constructor.proof

README.md

Taclet_bsum_num_of_eq0.proof

Taclet_bsum_num_of_gt1.proof

Taclet_seqPerm_existsLemma.proof

fr.up.xlim.sic.ig.jerboa.jme.model.JMEArc(fr.up.xlim.sic.ig.jerboa.jme.model.JMEArc__JMEArc(fr.up.xlim.sic.ig.jerboa.jme.model.JMENode,fr.up.xlim.sic.ig.jerboa.jme.model.JMENode,int)).JML normal_behavior operation contract.0.proof

fr.up.xlim.sic.ig.jerboa.jme.model.JMEArc(fr.up.xlim.sic.ig.jerboa.jme.model.JMEArc__getDimension()).JML normal_behavior operation contract.0.proof

fr.up.xlim.sic.ig.jerboa.jme.model.JMEArc(fr.up.xlim.sic.ig.jerboa.jme.model.JMEArc__oppositeNode(fr.up.xlim.sic.ig.jerboa.jme.model.JMENode)).JML normal_behavior operation contract.0.proof

fr.up.xlim.sic.ig.jerboa.jme.model.JMEArc(java.lang.Object___inv_()).JML accessible clause.0.proof

fr.up.xlim.sic.ig.jerboa.jme.model.JMEGraph(JMEGraph__existsValidPath(JMENode,JMENode,JerboaOrbit)).JML model_behavior operation contract.0.proof

fr.up.xlim.sic.ig.jerboa.jme.model.JMEGraph(JMEGraph__hasArc(JMENode,JMENode,JerboaOrbit)).JML model_behavior operation contract.0.proof

fr.up.xlim.sic.ig.jerboa.jme.model.JMEGraph(fr.up.xlim.sic.ig.jerboa.jme.model.JMEGraph__JMEGraph(fr.up.xlim.sic.ig.jerboa.jme.model.JMERule,boolean)).JML normal_behavior operation contract.0.proof

fr.up.xlim.sic.ig.jerboa.jme.model.JMEGraph(fr.up.xlim.sic.ig.jerboa.jme.model.JMEGraph__arcsAreInGraph()).JML accessible clause.0.proof

fr.up.xlim.sic.ig.jerboa.jme.model.JMEGraph(fr.up.xlim.sic.ig.jerboa.jme.model.JMEGraph__arcsAreInGraph()).JML model_behavior operation contract.0.proof

fr.up.xlim.sic.ig.jerboa.jme.model.JMEGraph(fr.up.xlim.sic.ig.jerboa.jme.model.JMEGraph__arcsAreUnique()).JML accessible clause.0.proof

fr.up.xlim.sic.ig.jerboa.jme.model.JMEGraph(fr.up.xlim.sic.ig.jerboa.jme.model.JMEGraph__arcsAreUnique()).JML model_behavior operation contract.0.proof

fr.up.xlim.sic.ig.jerboa.jme.model.JMEGraph(fr.up.xlim.sic.ig.jerboa.jme.model.JMEGraph__existsValidPath(fr.up.xlim.sic.ig.jerboa.jme.model.JMENode,fr.up.xlim.sic.ig.jerboa.jme.model.JMENode,up.jerboa.core.JerboaOrbit)).JML accessible clause.0.proof

fr.up.xlim.sic.ig.jerboa.jme.model.JMEGraph(fr.up.xlim.sic.ig.jerboa.jme.model.JMEGraph__getHooks()).JML normal_behavior operation contract.0.proof

fr.up.xlim.sic.ig.jerboa.jme.model.JMEGraph(fr.up.xlim.sic.ig.jerboa.jme.model.JMEGraph__getIncidentArcsFromNode(fr.up.xlim.sic.ig.jerboa.jme.model.JMENode)).JML normal_behavior operation contract.0.proof

fr.up.xlim.sic.ig.jerboa.jme.model.JMEGraph(fr.up.xlim.sic.ig.jerboa.jme.model.JMEGraph__getRule()).JML normal_behavior operation contract.0.proof

fr.up.xlim.sic.ig.jerboa.jme.model.JMEGraph(fr.up.xlim.sic.ig.jerboa.jme.model.JMEGraph__hasArc(fr.up.xlim.sic.ig.jerboa.jme.model.JMENode,fr.up.xlim.sic.ig.jerboa.jme.model.JMENode,up.jerboa.core.JerboaOrbit)).JML accessible clause.0.proof

fr.up.xlim.sic.ig.jerboa.jme.model.JMEGraph(fr.up.xlim.sic.ig.jerboa.jme.model.JMEGraph__hasCorrectDimensionsArcs(int)).JML accessible clause.0.proof

fr.up.xlim.sic.ig.jerboa.jme.model.JMEGraph(fr.up.xlim.sic.ig.jerboa.jme.model.JMEGraph__hasCorrectDimensionsArcs(int)).JML model_behavior operation contract.0.proof

fr.up.xlim.sic.ig.jerboa.jme.model.JMEGraph(fr.up.xlim.sic.ig.jerboa.jme.model.JMEGraph__hasCorrectDimensionsNodes(int)).JML accessible clause.0.proof

fr.up.xlim.sic.ig.jerboa.jme.model.JMEGraph(fr.up.xlim.sic.ig.jerboa.jme.model.JMEGraph__hasCorrectDimensionsNodes(int)).JML model_behavior operation contract.0.proof

fr.up.xlim.sic.ig.jerboa.jme.model.JMEGraph(fr.up.xlim.sic.ig.jerboa.jme.model.JMEGraph__isLeft()).JML normal_behavior operation contract.0.proof

fr.up.xlim.sic.ig.jerboa.jme.model.JMEGraph(fr.up.xlim.sic.ig.jerboa.jme.model.JMEGraph__isValidPath(_seq,fr.up.xlim.sic.ig.jerboa.jme.model.JMENode,up.jerboa.core.JerboaOrbit)).JML accessible clause.0.proof

fr.up.xlim.sic.ig.jerboa.jme.model.JMEGraph(fr.up.xlim.sic.ig.jerboa.jme.model.JMEGraph__nodesAreUnique()).JML accessible clause.0.proof

fr.up.xlim.sic.ig.jerboa.jme.model.JMEGraph(fr.up.xlim.sic.ig.jerboa.jme.model.JMEGraph__nodesAreUnique()).JML model_behavior operation contract.0.proof

fr.up.xlim.sic.ig.jerboa.jme.model.JMEGraph(fr.up.xlim.sic.ig.jerboa.jme.model.JMEGraph__orbit(fr.up.xlim.sic.ig.jerboa.jme.model.JMENode,up.jerboa.core.JerboaOrbit)).JML normal_behavior operation contract.0.proof

fr.up.xlim.sic.ig.jerboa.jme.model.JMEGraph(fr.up.xlim.sic.ig.jerboa.jme.model.JMEGraph__orbitIteration(java.util.List,java.util.Set,up.jerboa.core.JerboaOrbit)).JML normal_behavior operation contract.0.proof

fr.up.xlim.sic.ig.jerboa.jme.model.JMEGraph(fr.up.xlim.sic.ig.jerboa.jme.model.JMEGraph__orbitIterationPart(fr.up.xlim.sic.ig.jerboa.jme.model.JMENode,up.jerboa.core.JerboaOrbit,java.util.List)).JML normal_behavior operation contract.0.proof

fr.up.xlim.sic.ig.jerboa.jme.model.JMEGraph(fr.up.xlim.sic.ig.jerboa.jme.model.JMEGraph__removeAll(java.util.List,java.util.Collection)).JML normal_behavior operation contract.0.proof

fr.up.xlim.sic.ig.jerboa.jme.model.JMEGraph(java.lang.Object___inv_()).JML accessible clause.0.proof

fr.up.xlim.sic.ig.jerboa.jme.model.JMELoop(fr.up.xlim.sic.ig.jerboa.jme.model.JMEArc__getDimension()).JML normal_behavior operation contract.0.proof

fr.up.xlim.sic.ig.jerboa.jme.model.JMELoop(fr.up.xlim.sic.ig.jerboa.jme.model.JMEArc__oppositeNode(fr.up.xlim.sic.ig.jerboa.jme.model.JMENode)).JML normal_behavior operation contract.0.proof

fr.up.xlim.sic.ig.jerboa.jme.model.JMELoop(java.lang.Object___inv_()).JML accessible clause.0.proof

fr.up.xlim.sic.ig.jerboa.jme.model.JMENode(fr.up.xlim.sic.ig.jerboa.jme.model.JMENode__JMENode(fr.up.xlim.sic.ig.jerboa.jme.model.JMEGraph,java.lang.String,fr.up.xlim.sic.ig.jerboa.jme.model.JMENodeKind)).JML normal_behavior operation contract.0.proof

fr.up.xlim.sic.ig.jerboa.jme.model.JMENode(fr.up.xlim.sic.ig.jerboa.jme.model.JMENode__getGraph()).JML normal_behavior operation contract.0.proof

fr.up.xlim.sic.ig.jerboa.jme.model.JMENode(fr.up.xlim.sic.ig.jerboa.jme.model.JMENode__getKind()).JML normal_behavior operation contract.0.proof

fr.up.xlim.sic.ig.jerboa.jme.model.JMENode(fr.up.xlim.sic.ig.jerboa.jme.model.JMENode__getName()).JML normal_behavior operation contract.0.proof

fr.up.xlim.sic.ig.jerboa.jme.model.JMENode(java.lang.Object___inv_()).JML accessible clause.0.proof

fr.up.xlim.sic.ig.jerboa.jme.model.JMENodeKind(java.lang.Comparable__compareTo(java.lang.Object)).JML behavior operation contract.0.proof

fr.up.xlim.sic.ig.jerboa.jme.model.JMENodeKind(java.lang.Enum__getDeclaringClass()).JML behavior operation contract.0.proof

fr.up.xlim.sic.ig.jerboa.jme.model.JMENodeKind(java.lang.Enum__name()).JML behavior operation contract.0.proof

fr.up.xlim.sic.ig.jerboa.jme.model.JMENodeKind(java.lang.Enum__ordinal()).JML behavior operation contract.0.proof

fr.up.xlim.sic.ig.jerboa.jme.model.JMERule(fr.up.xlim.sic.ig.jerboa.jme.model.JMERule__getHooks()).JML normal_behavior operation contract.0.proof

fr.up.xlim.sic.ig.jerboa.jme.model.JMERule(fr.up.xlim.sic.ig.jerboa.jme.model.JMERule__hasHookIfNotEmpty()).JML accessible clause.0.proof

fr.up.xlim.sic.ig.jerboa.jme.model.JMERule(fr.up.xlim.sic.ig.jerboa.jme.model.JMERule__hasHookIfNotEmpty()).JML model_behavior operation contract.0.proof

fr.up.xlim.sic.ig.jerboa.jme.model.JMERule(java.lang.Comparable__compareTo(java.lang.Object)).JML behavior operation contract.0.proof

fr.up.xlim.sic.ig.jerboa.jme.model.JMERule(java.lang.Object___inv_()).JML accessible clause.0.proof

fr.up.xlim.sic.ig.jerboa.jme.verif.JMERuleErrorSeverity(java.lang.Comparable__compareTo(java.lang.Object)).JML behavior operation contract.0.proof

fr.up.xlim.sic.ig.jerboa.jme.verif.JMERuleErrorSeverity(java.lang.Enum__getDeclaringClass()).JML behavior operation contract.0.proof

fr.up.xlim.sic.ig.jerboa.jme.verif.JMERuleErrorSeverity(java.lang.Enum__name()).JML behavior operation contract.0.proof

fr.up.xlim.sic.ig.jerboa.jme.verif.JMERuleErrorSeverity(java.lang.Enum__ordinal()).JML behavior operation contract.0.proof

fr.up.xlim.sic.ig.jerboa.jme.verif.JMERuleErrorType(java.lang.Comparable__compareTo(java.lang.Object)).JML behavior operation contract.0.proof

fr.up.xlim.sic.ig.jerboa.jme.verif.JMERuleErrorType(java.lang.Enum__getDeclaringClass()).JML behavior operation contract.0.proof

fr.up.xlim.sic.ig.jerboa.jme.verif.JMERuleErrorType(java.lang.Enum__name()).JML behavior operation contract.0.proof

fr.up.xlim.sic.ig.jerboa.jme.verif.JMERuleErrorType(java.lang.Enum__ordinal()).JML behavior operation contract.0.proof

fr.up.xlim.sic.ig.jerboa.jme.verif.impl.JMEVerifTopoClassic(fr.up.xlim.sic.ig.jerboa.jme.verif.impl.JMEVerifTopoClassic__intersectionSize(java.util.Set,java.util.List)).JML normal_behavior operation contract.0.proof

fr.up.xlim.sic.ig.jerboa.jme.verif.impl.JMEVerifTopoClassic(fr.up.xlim.sic.ig.jerboa.jme.verif.impl.JMEVerifTopoClassic__verifNodeOrbitSizes(fr.up.xlim.sic.ig.jerboa.jme.model.JMERule)).JML normal_behavior block contract.0.proof

up.jerboa.core.JerboaOrbit(java.lang.Object___inv_()).JML accessible clause.0.proof

up.jerboa.core.JerboaOrbit(up.jerboa.core.JerboaOrbit__JerboaOrbit((I)).JML normal_behavior operation contract.0.proof

up.jerboa.core.JerboaOrbit(up.jerboa.core.JerboaOrbit__contains(int)).JML accessible clause.0.proof

up.jerboa.core.JerboaOrbit(up.jerboa.core.JerboaOrbit__contains(int)).JML normal_behavior operation contract.0.proof

up.jerboa.core.JerboaOrbit(up.jerboa.core.JerboaOrbit__get(int)).JML normal_behavior operation contract.0.proof

up.jerboa.core.JerboaOrbit(up.jerboa.core.JerboaOrbit__getMaxDim()).JML normal_behavior operation contract.0.proof

up.jerboa.core.JerboaOrbit(up.jerboa.core.JerboaOrbit__indexOf(int)).JML normal_behavior operation contract.0.proof

up.jerboa.core.JerboaOrbit(up.jerboa.core.JerboaOrbit__makeCC(int)).JML normal_behavior operation contract.0.proof

up.jerboa.core.JerboaOrbit(up.jerboa.core.JerboaOrbit__size()).JML accessible clause.0.proof

up.jerboa.core.JerboaOrbit(up.jerboa.core.JerboaOrbit__size()).JML normal_behavior operation contract.0.proof

up.jerboa.core.JerboaOrbit(up.jerboa.core.JerboaOrbit__tab()).JML normal_behavior operation contract.0.proof

up.jerboa.core.JerboaOrbit(up.jerboa.core.JerboaOrbit__verifyDimensions(int)).JML accessible clause.0.proof

up.jerboa.core.JerboaOrbit(up.jerboa.core.JerboaOrbit__verifyDimensions(int)).JML model_behavior operation contract.0.proof

verifDimension.proof

verifDimensionGraphArcs.csv

verifDimensionGraphArcs.proof

verifDimensionGraphNodes.proof

verifDuplicateNode.csv

verifDuplicateNode.proof

verifDuplicateNodeGraph.csv

verifDuplicateNodeGraph.proof

verifHooks.proof

verifHooksForNode.proof

verifHooksFullOrbit.csv

verifHooksFullOrbit.proof

verifNodeOrbitSizes.proof

verifNodeOrbitSizesList.proof

Case study: verifying Jerboa's rule analyzer using KeY

src contains a KeY-verified fork of Jerboa's modeler editor static rule analyzer.

Used KeY version: https://github.com/FliegendeWurst/key/commit/a2f03f4b8f29184dd8b0d107edb6876965b02f95

This is based on a November 2025 commit with these PRs applied:

About

No description, website, or topics provided.

0 stars

0 watching

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Repository files navigation

Case study: verifying Jerboa's rule analyzer using KeY

About

Uh oh!

Releases

Packages

Uh oh!

Contributors

Uh oh!

Languages

Uh oh!

Folders and files

Latest commit

History

Repository files navigation

Case study: verifying Jerboa's rule analyzer using KeY

About

Resources

Uh oh!

Stars

Watchers

Forks

Releases

Packages 0

Uh oh!

Contributors

Uh oh!

Languages

Packages