US 8,413,119 B2 · Semantic subtyping for declarative data scripting language by calling a prover

Abstract

An efficient, logical and expressive type system supports the combination of refinement types and type membership expressions, as well as a top type that encompasses all valid values as members. Various embodiments verify the validity of subtyping relationships by translating to first-order logic, and invoking a general-purpose theorem prover with the first-order logic as input. In contrast to treating formulas as types, types are translated into formulas of standard first-order logic. Moreover, to represent data structures of the programming language as first-order logic, universal and existential quantifiers of first-order logic, and function symbols in terms, are exploited. Data intensive applications can be generated, verified, and deployed with greater speed and scale.

Claims20

Dependent claims

A method for validating at least a portion of a declarative program based on a background theory for a programming language having a type system that supports type test and refinement, including:

for a given environment, translating, by a computing device, a programming construct of the declarative program to at least one first order logic formula construct based on a semantic analysis;
determining, by the computing device, a validity of the at least one first order logic formula construct based on an analysis of the at least one first order logic formula construct;
and
determining, by the computing device, whether a first type of the programming construct is a valid subtype of a second type of the programming construct based on the validity determination, including:
forming, for each type T, a formula F[T](x) that is true if and only if x is a value of type T;
and
checking whether a type S is a subtype of the type T through use of a formula of the form (∀x. F[S](x)=F[T](x)).

4 more elements

A computer system, including:

a system memory and a processor that are respectively configured to store and execute instructions, including instructions organized into:
at least one declarative code module comprising computer executable instructions representative of declarative code according to a declarative programming model implementing a type system supporting constraint-based refinement type statements and type test statements in the refinement type statements, the at least one declarative code module including a plurality of programming constructs;
and
a declarative code interpretation module for interpreting and verifying validity of the plurality of constructs according to rules defined based on the type system, wherein the declarative code interpretation module transforms expressions including subtyping relationships to first order logic terms and formulas and invokes at least one prover to test a validity of the first order logic terms and formulas to inform whether the subtyping relationships are valid wherein, for a type T, the declarative code interpretation module forms a formula F[T](x) that holds if and only if x is a value of type T, and wherein the declarative code interpretation module checks whether a type S is a subtype of the type T by generating a formula of the form (∀x. F[S](x)=F[T](x)).

1 more element

Dependencies are inferred from the claim text.

Semantic subtyping for declarative data scripting language by calling a prover

Life of this patent

Semantic subtyping for declarative data scripting language by calling a prover

Life of this patent

Abstract

Claims20