Skip navigation links

Package de.uka.ilkd.key.speclang.njml

This package provides the functionalities of parsing JML comments into KeY constructs.

See: Description

Package de.uka.ilkd.key.speclang.njml Description

This package provides the functionalities of parsing JML comments into KeY constructs. JmlIO is the entry facade for the end-developer.

The main translation happens (due to legacy restriction) in two step: First the given comments are parsed and wrapped into TextualJML* part. Second these are interpreted and attached to the SpecificationRepository This process happens in the legacy package de.uka.ilkd.key.speclang.jml.

The translation happens in TextualTranslator and Translator.

Gradle has a task for debugging the lexer gradle debugJmlLexer.

Skip navigation links

Copyright © 2003-2019 The KeY-Project.