High-assurance User-defined Functions

Many data integration tasks require user defined functions (UDFs): for example, to convert inches to centimeters. When UDFs are defined or used incorrectly, data can be silently corrupted. In AQL, user-defined functions are first-class schema elements, and AQL's automated theorem proving technology seamlessly provides high-assurance compile-time aid to schemas with user-defined functions.

This example (built in to the IDE with name Unit Conv) defines a source schema about American airplanes, which have wing spans in inches, and a target schema about European airplanes, which have wing spans in centimeters. The type side specifies how to convert inches to centimeters, and a query which does not convert inches to centimeters is rejected. Although this example uses a relatively simply type conversion, AQL supports user-defined types defined by arbitrary equations.

We start by defining a type side that contains two user defined types, inches and centimeters, as well as a conversion between them:

typeside Ty = literal { java_types in = "java.lang.Double" cm = "java.lang.Double" java_constants in = "return java.lang.Double.parseDouble(input[0])" cm = "return java.lang.Double.parseDouble(input[0])" java_functions inToCm : in -> cm = "return (2.54 * input[0])" }


The source and target schemas contain wingspans in inches (for American planes) and centimeters (for European planes):

schema AmericanAirplane = literal : Ty { entities Wing attributes wingLength : Wing -> in } schema EuropeanAirplane = literal : Ty { entities Wing attributes wingLength : Wing -> cm }


An American airplane instance is, for example:

instance Boeing747 = literal : AmericanAirplane { generators left right : Wing equations left.wingLength = right.wingLength left.wingLength = 500 }

unitconv1

To convert an American airplane to a European airplane requires converting inches to centimeters:

query AmericanToEuropean = literal : AmericanAirplane -> EuropeanAirplane { entities Wing -> {from w:Wing return wingLength -> inToCm(w.wingLength)} } instance Boeing747Metric = eval AmericanToEuropean Boeing747

unitconv2

A similar query that omits the unit conversion is rejected:

query AmericanToEuropean_disastrous_conversion = literal : AmericanAirplane -> EuropeanAirplane { entities Wing -> {from w:Wing return wingLength -> w.wingLength} } Error in query AmericanToEuropean_disastrous_conversion: in attribute wingLength, expected sort of wingLength(w) is cm but wingLength(w) actually has sort in.


A screen shot of the entire development is shown below:

unitconv3