INKA generates proof obligations from (CASL-) specifications and assists in finding proofs for them. It exploits the logical content of a specification and special strategic knowledge computed from the logical content. It does not directly use comments. The following brief description shows, how it manages to display comments to the user even if these are not represented in the AST the frontent produces.
In the INKA 5.0 frontend, each lexeme (excluding comments and special purpose annotations) is returned by the lexer together with its start and end positions in the input text (i.e. their line/column numbers and character count in the file). These positions are inherited whenever the parser constructs an AST from its constituents. When creating the prover's internal representation of the input, each sort symbol or axiom, say, is stored together with its position in the input text. Thus given a symbol or a formula from the specification it is possible to display the original text to the user. Of course this presentation will not pretty print the text but rather show the original ASCII version, which includes all annotations and comments that were in the input text.
According to our experiences this is an efficient way of working on specifications when the specifications change frequently, which is the case in the scenario of the INKA system.