Skip to content

UnderstandingLanguages

Jump to bottom
Kassing edited this page Mar 30, 2026 · 1 revision

Supported Languages

Currently, AProVE supports a range of languages defined in the aprove.verification.oldframework.Input.Language enumeration, including:

  • TES, TRS, PTRS, CSR, FP, IPAD, JAVA, PROLOG, HASKELL, And others...

In addition, various analyses are available as defined in aprove.verification.oldframework.Input.HandlingMode, such as:

  • Termination analysis
  • Liveness analysis
  • Safety analysis
  • Theorem proving

Supported Language and Analysis Combinations

Not all combinations of languages and analyses are supported. For example:

  • Termination analysis is available for nearly all supported input languages.
  • Theorem proving is only supported for FP.
  • Liveness analysis is only available for TRS.

Adding a New Language

Integrating a new language into the AProVE system involves a few steps. Let’s assume the new language is YATRS (Yet Another Term Rewrite System). The following steps outline the basic process. You can always compare these steps to the existing classes and code snippets for ordinary term rewrite systems, indicated by the brackets.

1. Add a New Parser

To add a new parser for the YATRS language, follow these steps:

  • Grammar: Create an ANTLR (preferred) or SableCC grammar for the language. The grammar files should be placed in src/aprove/input/Grammars. (NewTrs.g)
  • Build: Modify the build-aprove.xml file to include the new grammar. (target: newTrs)
  • Generated Files: The files generated by the parser generator will reside in gen/aprove/input/Generated. (NewTrsParser)
  • Parser: Implement the translator in src/aprove/input/Programs that translates the parsed input (RawTrs) given by the generated parser (NewTrsParser) into the correct problem class (TRSProblem). (src/aprove/input/Programs/newTrs/Translator.java)

2. Add a New Problem Class

Create a new problem class for YATRS. The steps include:

  • Add YATRS to the aprove.verification.oldframework.Input.Language enum.
  • Add the translator to the verification.oldframework/Input/extension.properties file.
  • Modify aprove.verification.theoremprover.ObligationFactories.MetaObligationFactory to include a case for Language.YATRS.
  • Write a (possibly empty) YATRSAnnotation class in aprove.verification.oldframework.Input.Annotations.
  • Add the line "YATRS = aprove.verification.oldframework.Input.Annotators.YATRSAnnotator" to aprove.verification.oldframework.Input.Annotators.defaultannotators.properties.

3. Create Processors for the New Problem Class

Develop processors for the YATRS problem class. The following steps outline the basic process:

  • Write a processor (e.g., YATRSToQTRS) to transform YATRS into QTRS.
  • Add the new processor (e.g., YATRSToQTRS) to aprove.predefinedstrategies.Modules.std.strategy.
  • Update the default strategy in aprove.predefinedstrategies.Auto.current.strategy to use this processor by default.

Optional Steps (Can be ignored if you do not urgently need them)

Depending on the complexity of your problem, you may need to perform additional steps:

4. Special Output for Proof Header

Note: The FrameProof/FrameProofFactory classes referenced here no longer exist in the codebase. This step may be obsolete or have changed. Check current proof header handling before following this guidance.

If your problem requires special output for the "this problem has been proven (/disproven)" header in the proof output, you should:

  • Implement the getProofResult() method on your problem's proof class.

5. Annotations

If your problem requires non-trivial annotations:

  • Add a new annotation class (e.g., YATRSAnnotation) in aprove.verification.oldframework.Input.Annotations.
  • Implement a corresponding Annotator in aprove.verification.oldframework.Input.Annotators.

If no special annotation is needed, the default TrivialAnnotator.TrivialAnnotation will be used.

6. Add a Case for Heuristic Processors

Add a case in relevant heuristic processors for the new language (e.g., YATRS).

7. Citations

If required, add citations for your problem in aprove.verification.oldframework.Utility.Citation.

Optional UI (Possibly Outdated)

If you need to display a graph or provide additional UI functionality for your new language, follow these optional steps:

8. Displaying a Graph

To display a graph in the proof window:

  • Implement the DOT_Able interface.
  • Add the new file type to GraphUserInterface/Kefir/filefilters.properties.
  • Add it to the _SAVENORM property if you want to enable saving files of that type.

9. Displaying Options for the Problem

To display problem-specific options:

  • Add a new class to GraphUserInterface/Kefir/TypedOptionPanels.
  • Register the class in GraphUserInterface/Kefir/optionsManager.properties. If you don’t want to add a specific class, use the default option.

10. Customizing the 'Display Problem' Window

To customize the "display problem" window:

  • Add a new InteractiveObligationPanel in GraphUserInterface/Interactive.
  • Add this panel to GraphUserInterface/Interactive/ObligationPanelFactory. If this step is skipped, the default InteractiveDefaultPanel will be used.

11. Implementing ExternUsable Interface

If you want to offer a "Save problem source" button or make your problem processable by an external processor:

  • Implement the ExternUsable interface.

12. Configuring Processors

To make processors interactively available for your problem:

  • Configure a list of processors in aprove.GraphUserInterface.Options.OptionsItemsFactories.\$MYPROBLEM.properties.

This allows users to apply processors to your problem interactively (e.g., via the "Apply processor" option in the context menu).

Clone this wiki locally