Informal and Formal Specifications:

The Next Phase

Aarne Ranta, Hans-Joachim Daniels, Kristofer Johannisson

aarne@cs.chalmers.se, daniels@ira.uka.de, krijo@cs.chalmers.se

KeY Workshop, Königswinter, 7-10 June 2004 Overview KeY-GF: current status Interactive editing vs. batch translation From enemy to friend: let definitions Support for German API for annotations

KeY mission Introduce formal methods into every-day software engineering.

GF mission Introduce natural-language technology into everyday programming.

Joint KeY-GF mission Bridge the gap between formal and informal specifications.

Language technology for programmers

Enable high-qualigy natural language treatment in programs

error messages: your program has 1 syntax errors
localization: dein Program hat 57 Syntaxfehler

interaction with speech and text documentation Relevant characteristics of GF Not just a system, but produces components Grammars are declarative and therefore portable Grammar writing is similar to compiler construction Grammar engineering is similar to software engineering GF and compiler construction Reminder:

grammar = abstract syntax + concrete syntaxes parsing = from string to abstract syntax tree linearization = from abstract syntax tree to string

Linearization rules are similar to compositional compilation schemes Compiler in GF: example

Abstract syntax, Java expressions, and JVM bytecode

fun ESum : Exp -> Exp -> Exp ;
fun EInt : Int -> Exp ;
lin ESum x y = {s = x.s ++ "+" ++ y.s}
lin EInt i   = i ;
lin ESum x y = {s = x.s ++ y.s ++ "iadd" ++ ";"}
lin EInt i   = {s = "bipush" ++ i.s ++ ";"} ;

Compilation example

56 + 89                        -- Java source
ESum (EInt 56) (EInt 89)       -- syntax tree
bipush 56 ; bipush 89 ; iadd ; -- generated JVM

GF is a functional programming language

Grammars are not just string manipulation, but there are datatypes and datastructures, and one can define function libraries, e.g.

param Precedence = P1 | P2 | P3 | P4 | P5 | P6 ;
oper Term : Type = {s : Str ; p : Precedence} ;
oper infixl : Precedence -> Str -> Term -> Term -> Term = ... ;
oper const : Precedence -> Str -> Term = ... ;

So now one can write

lin ESum = infixl P5 "+" ;
lin EInt = const P6 ;

Compiling natural language View natural language in the same way as a formal language:

abstract syntax formal semantics compilation techniques

This works well for limited language fragments .

Compiling natural language: examples Relatively simple for English

  lin ESum x y = {s = ["the sum of"] ++ x.s ++ "and" ++ y.s}

More involved for German…

  lin ESum x y = {s = table {
    Nom => ["die Summe von]"  ; x.s ! Dat ++ "und" ++ y.s ! Dat ;
    Gen => ["der Summe von]"  ; x.s ! Dat ++ "und" ++ y.s ! Dat ;
    ...}}

… but made simple by suitable library functions:

  lin ESum x y = funColl (mkFunVon (nFrau "Summe")) x y ;

KeY-GF Specifications are a promising field for GF:

limited language with intended semantics programmers as grammar engineers

Currently the largest GF application related to programming.

The current system Work started in 2001 (Hähnle, Johannisson, Ranta). Straighforward idea: bilingual GF grammar with OCL and English as concrete syntaxes. Two working modes

interactive authoring

batch translation from OCL to English

(translation from English to OCL considered unrealistic)

Most work has been on interactive authoring.

The abstract syntax We exploit the ideas of type-theoretical proof editors,

dependent types Higher-Order Abstract Syntax (HOAS)

to derive an editor that guarantees well-formedness: correct typing of method applications control of what variables are in scope Abstract syntax examples

cat Class ;
cat Instance Class ;
cat VarSelf Class ;
fun floor : Instance Real -> Instance Integer;
fun self  : (c : Class) -> VarSelf c -> Instance c ;
fun Inv   : (c : Class) -> (VarSelf c -> ConstraintBody) -> Constraint ;

Pluralistic editing Top-down:

refinements from menus refinement by parsing

Bottom-up:

local and grobal wrapping clipboard The editor behaviour is entirely generic, using type checking with metavariables (Coquand) and a tree zipper (Huet).

Problems with strongly typed abstract syntax Scale-up is not perfect:

full OCL is difficult to cover

big documents are tedious to write by editing feedback to user gets unintuitive

Example: HOAS for let definitions with parameters has to encode function types and argument lists syntactically. It is theoretically interesting that this can be done, but the abstract syntax is complex and unintuitive.

Constructing let definitions with parameters

cat
Class   ; Instance  Class ;
Classes ; Instances Classes ;
LetDef Classes Class ;
fun
CNil  : Classes ;
CCons : Class -> Classes -> Classes ;
INil  : Instances CNil ;
ICons : (c : Class) -> (cs : Classes) ->
          Instance c -> Instances cs -> Instances (CCons c cs)  ;
Let   : (cs : Classes) -> (c : Class) ->
          (Instances cs -> Instance c) -> LetDef cs c ;

Using let definitions with parameters

fun
ELet  : (cs : Classes) -> (c : Class) -> (e : Class) ->
          LetDef cs c -> (LetDef cs c -> Instance e) -> Instance e ;
rfLet : (cs : Classes) -> (c : Class) ->
          LetDef cs c -> Instances cs -> Instance c ;
headI : (c : Class) -> (cs : Classes) ->
          Instances (CCons c cs) -> Instance c ;
tailI : (c : Class) -> (cs : Classes) ->
          Instances (CCons c cs) -> Instances cs ;

Example syntax tree of a let expression

let step(x) = x + 2 in
step(5)
ELet (CCons Integer CNil) Integer Integer
(Let (CCons Integer CNil) Integer
  (\x -> EPlus
          (headI Integer CNil x)
          (EInt 2)
  )
)
(\step -> rfLet (CCons Integer CNil) Integer
            step
            (ICons Integer CNil (EInt 5) INil)
)

The parsing problem Subclass coercion in OCL is treated with the rule

  fun coerce : (c,d : Class) -> Subtype c d -> Instance c -> Instance d ;
  lin coerce ___obj = obj ;

Parsing is done via translation to a context-free skeleton (“off-line parsing”), which becomes cyclic

  coerce. Instance ::= Instance

making the parser to loop with infinitely many results. This has been solved in a general way for GF (Peter Ljunglöf).

Why not parse OCL in GF Ordinary (compiled) parsing is more efficient than GF parsing. We want a full-coverage OCL grammar. Compositional translation does not give good enough text quality. It is often enough to translate OCL files in batch mode.

Intermediate conclusion Batch translation and interactive editing need partly different approaches.

Strategy for batch translation Abstract syntax for OCL

the “normal” one, defined in BNF complete, following OCL 1.4

Abstract syntax for natural language richer, with alternative textual forms common for English and German (although not necessarily)

Translation from OCL to natural language

OCL parser derived by BNF Converter OCL type checker (in Haskell) GF code generator (in Haskell)

Optimizing translation Translation is optimizing, not compositional Hence it cannot be defined directly in GF Strategies:

instruction selection by case analysis

back-end optimization passes (peephole etc) (Also cf. methods of NLG (Natural Language Generation))

Examples of optimization Syntactic category distinctions

Instance Bool: the condition that the lift goes down is false Sent: it is not the case that the lift goes down AtomSent: the lift does not go down

Referring expression generation: the age of the person — the age — it Much more could be done as back-end passes.

Another example of optimization

Grouping of conjuncts (aggregation):

the card is presented or the price is more than 50 and the price is less than 100

the card is presented or the price is more than 50 and less than 100

Notice: aggregation is useful in disambiguation, because connectives between parts of sentences bind stronger than connectives between whose sentences.

User-defined vocabulary This is the most important stylistic improvement Use the same vocabulary as in the informal specification… … instead of vocabulary derived by default Sources of user-defined vocabulary:

the UML model: classes, attributes, properties let definitions let definitions in OCL The mechanism of top-level definitions (“macros”) of OCL (thus misleading keyword) Two advantages for text generation

extend user-defined vocabulary structure the code better

Reminder: NL bears syntactic complexity much worse than OCL!

Example: a text without lets (from XFST)

To mark the end of every string that begins with an optional sequence of symbols from the list ‘d’, ‘g’, ‘h’, ‘j’, ‘k’, ‘l’, ‘m’, ‘n’, ‘p’, ‘r’, ‘s’, ‘t’, ‘v’ and continues by a nonempty sequence of symbols from the list ‘a’, ‘e’, ‘i’, ‘o’, ‘u’, ‘y’ followed by an optional sequence of symbols from the list ‘b’, ‘c’, ‘d’, ‘f’, ‘g’, ‘h’, ‘j’, ‘k’, ‘l’, ‘m’, ‘n’, ‘p’, ‘q’, ‘r’, ‘s’, ‘t’, ‘v’ by ‘-’ if it is followed by a string that begins with an optional sequence of symbols from the list ‘b’, ‘c’, ‘d’, ‘f’, ‘g’, ‘h’, ‘j’, ‘k’, ‘l’, ‘m’, ‘n’, ‘p’, ‘q’, ‘r’, ‘s’, ‘t’, ‘v’ and continues by a nonempty sequence of symbols from the list ‘a’, ‘e’, ‘i’, ‘o’, ‘u’, ‘y’, choosing the longest matches from left to right.

The same text with lets

A vowel is a symbol from the list ‘a’, ‘e’, ‘i’, ‘o’, ‘u’, ‘y’.

A consonant is a symbol from the list ‘b’, ‘c’, ‘d’, ‘f’, ‘g’, ‘h’, ‘j’, ‘k’, ‘l’, ‘m’, ‘n’, ‘p’, ‘q’, ‘r’, ‘s’, ‘t’, ‘v’.

A syllable is a string that begins with an optional sequence of consonants and continues by a nonempty sequence of vowels followed by an optional sequence of consonants.

To hyphenate is to mark the end of every syllable by ‘-’ if it is followed by a string that begins with a consonant and continues by a vowel, choosing the longest matches from left to right.

Code generation for lets (In OCL 1.4) Group let definitions and the rest of the constraint in a special data structure. Display the let definitions along with the rest of the text. The let-defined constants are global in the GF grammar:

would destroy type correctness in editing but does not matter in batch translation The grammar of natural language Core grammar + user-defined grammar User-defined grammar comes from two sources

UML model let definitions

Abstract syntax is derived automatically Concrete has two options linearization rules generated by default annotations overriding the defaults GF 2.0: GF with a module system The user-defined grammar is an extension of the core grammar The core grammar has been compiled separately = ⇒ shorter start-up time Resource grammars: library modules that hide linguistic details and guarantee grammaticality by type system Grammar engineering in GF Resource grammarians

linguistic knowledge about a language no particular domain but “the whole language”

Application grammarians semantic knowledge of domain practical knowledge of target language Grammar engineering for specifications The “second version” of the core NL grammar grammar: an application grammar using the resource library (Hans-Joachim Daniels). User-defined annotations define an extended application grammar (much simpler than the core). Goal: writing annotations should be made very easy!

The GF resource grammar library Complete morphology (parameters, inflectional patterns) Syntax for technical texts and simple dialogues English, Finnish, French, German, Italian, Russian, Swedish Language-independent API for syntax Language-dependent APIs for morphology and lexicon Core grammar examples Share structures between English and German

fun otAttributes : Instance OclType -> Instance (Set StringC);
lin otAttributes t = np2inst (appFun1 (funOfCN (AppFun (funGen setN)
  (DefM anyNP (AppFun (funGen nameN) (DefManyNP (UseN  attributeN))))))
  (inst2np t)) ;

The vocabulary definitions differ, of course:

oper setN : N = nFrau "Menge";    -- German
oper setN : N = nNonhuman "set";  -- English

The translations are structurally very similar: die Menge der Namen der Attribute von dem OCL-Typ the set of the names of the attributes of the OCL type Language-independent resource syntax API (fragment)

predV1 : V -> NP -> AS ;             -- one-place verb:      "John walks"
predV2 : TV -> NP -> NP -> AS ;      -- two-place verb:      "John loves Mary"
predV3 : V3 -> NP -> NP -> NP -> AS ;-- three-place verb:    "John prefers Mary to Jane"
predVColl : V -> NP -> NP -> AS ;    -- collective verb:     "John and Mary fight"
predA1 : Adj1 -> NP -> AS ;          -- one-place adjective: "John is old"
predA2 : Adj2 -> NP -> NP -> AS ;    -- two-place adj:       "John is married to Mary"
predAColl : Adj1 -> NP -> NP -> AS ; -- collective adj:      "John and Mary are married"
predN1 : CN -> NP -> AS ;            -- one-place noun:      "John is a man"
predN2 : Fun -> NP -> NP -> AS ;     -- two-place noun:      "John is a lover of Mary"
predNColl : CN -> NP -> NP -> AS ;   -- collective noun:     "John and Mary are lovers"
predAdv : AdV -> NP -> AS ;          -- adverb:              "John is outside"
appFun1 : Fun -> NP -> NP ;          -- one-place function:  "the successor of x"
appFun2 : Fun2 -> NP -> NP -> NP ;   -- two-place function:  "the distance from x to y"
appFunColl : Fun -> NP -> NP -> NP ; -- collective function: "the sum of x and y"

German resource morphology API (fragment)

nRaum   : (_,_: Str) -> N ;           -- Raum, (Raumes,) Räume (masc)
nBuch   : (_,_: Str) -> N ;           -- Buch, (Buches, Bücher) (neut)
nAuto   : Str -> N ;                   -- Auto, (Autos, Autos) (neut)
nHand   : (_,_: Str) -> N ;           -- Hand, Hände; Mutter, Mütter (fem)
nFrau   : Str -> N ;                   -- Frau (,Frauen) ; Wiese (,Wiesen) (fem)
mkFun   : N -> Prep -> Case -> Fun ;   -- Nachfolger, von, dative
mkAdj1  : (_,_: Str) -> Adj1 ;        -- teuer, teur
mkAdj2  : Adj1 -> Str -> Case -> Adj2; -- teilbar, durch, accusative
vReg    : Str -> V ;                   -- führen
vSein   : V ;                          -- (sein)
mkVPart : V -> Str -> V ;              -- vFahren, aus

Annotation examples: German

concrete LiftGer of Lift = oclLibraryGer **
open ResourceGer, ParadigmsGer, LogicGer in {
lin Lift     = mkClass (UseN (nRaum "Fahrstuhl" "Fahrstühle")) "Lift" ;
lin Person   = mkClass (UseN (nFrau "Person")) "Person" ;
lin Office   = mkClass (UseN (nAuto "Büro")) "Office" ;
lin Level    = mkClass (UseN (nFrau "Stufe")) "Level" ;
lin Floor    = appFun1 (mkFun (nFrau "Stufe") "" nominative) ;
lin GoUp     = predV1  (mkVPart vFahren "hoch") ;
lin GoDown   = predV1  (mkVPart vFahren "herunter") ;
lin GoFromTo = predV3  (mkV3 vFahren "von" dative "zu" dative) ;
lin Capacity = appFun1 (funVon ((nFrau "Kapazität"))) ;
lin Admin    = appFun1 (mkFun ((nFehler "Verwalter")) [] genitive) ;
lin Distance = appFunColl (mkFun (nFrau "Entfernung") "zwischen" dative) ;
lin OutOfOrd = predAdv (mkAdV ["außer Betrieb"]) ;
lin Slow     = predA1  (adjGen "langsam") ;
lin CloseTo  = predA2  (mkAdj2 (adjGen "nahe") "bei" dative) ;
}

Forthcoming: example-based grammar writing Idea: instead of a linearization rule, write an example Parse the example with the resource grammar and generate the linearization rule This is how it can look like:

  GoUp x       = #parse "x fährt hoch"
  Distance x y = #parse "die Entfernung zwischen x und y"

Then we can say that only practical knowledge of German is needed!

Forthcoming: integration in KeY The batch translator can also be used as a stand-alone program Alternatives for the editor:

current model: separate GF process

deeper integration: use Java modules generated from GF

    (gramlets)

Not yet in Java:

OCL type checker and optimizing translator GF type checker with dependent types GF grammar compiler for annotations Conclusion Soon:

comprehensive batch translator from OCL to English and German APIs for annotations Later:

improved, pluralistic editing grammar writing by example

Some time in future?: GF functionality in Java modules