A Controlled Language for Software Specifications & Mathematical text
Muhammad Humayoun · 2010
Syntax Syntactic structure/tree cat Prop, Type, Property, Quant fun MkProp : Subj→ Quant→ [Property]→ Type→ Prop Two : Quant Even : Property Integer : Type . . . We deduce that x + y = 2(a + b) by the last statement. Thus x + y is an even integer because it is a multiple of 2. Concrete Syntax Linearization rules to each function Number = Sg | Pl Property, Quant, Prop = {s : Str} Type = {s : Number => Str} Two = “two” Integer = table {Sg => “integer” ; Pl => “integers” } Even = “even” MkProp subj quant props type = subj.s ++ be.s!subj.n ++ quant.s ++ props.s ++ type.s!subj.n Muhammad Humayoun A Controlled language for Software Specifications & Mathematical text 20/ 29 Motivation Examples Implementation details 1. Syntax Modular structure of the grammar allows to rephrase sentences We deduce that x + y = 2(a + b) by the last statement. By the last statement, we deduce that x + y = 2(a + b). By the last statement, x + y = 2(a + b) holds. By the last statement, x + y = 2(a + b). x + y = 2(a + b) by the last statement. Muhammad Humayoun A Controlled language for Software Specifications & Mathematical text 21/ 29 Motivation Examples Implementation details Automatic formalisation in three steps Muhammad Humayoun A Controlled language for Software Specifications & Mathematical text 22/ 29 Motivation Examples Implementation details 2. Semantics Building discourse Theorem. If x and y are two even integers then x + y is even. Proof. Suppose that x and y are two even integers. By the definition of even numbers, x + y = 2a + 2b holds. We deduce that x + y = 2(a + b) by the last statement. Thus x + y is an even integer because it is a multiple of 2. Variables Type Gender Number How Decl 2 (NoType Neut Sg DeclMan) it (? ? ? ?) x + y (Int Neut Sg DeclMan) x , y (Int Neut Pl DeclMan) a, b (NoType Neut Pl DeclAuto) x , y (Int Neut Pl DeclMan) x , y (Int Neut Pl DeclMan) x + y (NoType Neut Sg Prv) x , y (Int Neut Pl Prv) Muhammad Humayoun A Controlled language for Software Specifications & Mathematical text 23/ 29 Motivation Examples Implementation details 2. Semantics Solving basic anaphora e.g. It and They Theorem. If x and y are two even integers then x + y is even. Proof. Suppose that x and y are two even integers. By the definition of even numbers, x + y = 2a + 2b holds. We deduce that x + y = 2(a + b) by the last statement. Thus x + y is an even integer because it is a multiple of 2. Variables Type Gender Number How Decl 2 (NoType Neut Sg DeclMan) x + y (Int Neut Sg DeclMan) x + y (Int Neut Sg DeclMan) x , y (Int Neut Pl DeclMan) a, b (NoType Neut Pl DeclAuto) x , y (Int Neut Pl DeclMan) x , y (Int Neut Pl DeclMan) x + y (NoType Neut Sg Prv) x , y (Int Neut Pl Prv) Muhammad Humayoun A Controlled language for Software Specifications & Mathematical text 24/ 29 Motivation Examples Implementation details 2. Semantics Solving basic anaphora e.g. references Theorem. If x and y are two even integers then x + y is even. Proof. Suppose that x and y are two even integers. By the definition of even numbers, x + y = 2a + 2b holds. We deduce that x + y = 2(a + b) by the last statement. Thus x + y is an even integer because it is a multiple of 2. Formulas Type x + y ∈ Z & even (x + y ) Deduction x + y = 2(a + b) Deduction x + y = 2a + 2b Deduction x , y ∈ Z & (even (x) & even (y )) Hypothesis ∀x,y (x , y ∈ Z & even (x) & even (y ) ⇒ even (x + y )) Goal Muhammad Humayoun A Controlled language for Software Specifications & Mathematical text 25/ 29 Motivation Examples Implementation details 2. Semantics Distributive vs. Collective readings e.g. x and y are positive vs. x and y are equal positive(x) & positive(y) vs. equal(x,y) Translation of controlled language to an abstact mathematical langauge MathAbs Muhammad Humayoun A Controlled language for Software Specifications & Mathematical text 26/ 29 Motivation Examples Implementation details 2. Semantics Distributive vs. Collective readings e.g. x and y are positive vs. x and y are equal positive(x) & positive(y) vs. equal(x,y) Translation of controlled language to an abstact mathematical langauge MathAbs Muhammad Humayoun A Controlled language for Software Specifications & Mathematical text 26/ 29 Motivation Examples Implementation details 2. Semantics Distributive vs. Collective readings e.g. x and y are positive vs. x and y are equal positive(x) & positive(y) vs. equal(x,y) Translation of controlled language to an abstact mathematical langauge MathAbs Muhammad Humayoun A Controlled language for Software Specifications & Mathematical text 26/ 29 Motivation Examples Implementation details Automatic formalisation in three steps Muhammad Humayoun A Controlled language for Software Specifications & Mathematical text 27/ 29 Motivation Examples Implementation details 3. Verification MathAbs to first order formulas in progress . . . MathAbs to a prover specific formalism after PhD Logical types and linguistic types are not the same Need a theorem prover that could deals with types as predicates e.g. PMLa http://www.lama.univ-savoie.fr/tracpml Muhammad Humayoun A Controlled language for Software Specifications & Mathematical text 28/ 29 Motivation Examples Implementation details 3. Verification MathAbs to first order formulas in progress . . . MathAbs to a prover specific formalism after PhD Logical types and linguistic types are not the same Need a theorem prover that could deals with types as predicates e.g. PMLa http://www.lama.univ-savoie.fr/tracpml Muhammad Humayoun A Controlled language for Software Specifications & Mathematical text 28/ 29 Motivation Examples Implementation details Summary Specifications and Math text are similar problems A controlled language could work for both A long term working project, but feasible Muhammad Humayoun A Controlled language for Software Specifications & Mathematical text 29/ 29 Motivation Examples Implementation details Questions