Dminor

About

Dminor is a typechecker and interpreter for a first-order functional language, based on a subset of the code name "M" modeling language. Dminor is research software aimed at demonstrating the ideas of a type system based on interpreting types as formulas in first-order logic, and of checking the subtype relation during typechecking by calling an external SMT solver. In particular, Dminor relies on and comes with the Z3 solver.

A research paper describing a preliminary version of this software is available here.

The developers of Dminor are Gavin Bierman, Andrew D. Gordon, Catalin Hritcu, and David Langworthy.

Getting and Installing Dminor

Dminor is available as a download from the Microsoft Research website. The installer situates the binary and other execution files at C:\Program Files\Microsoft Research\Dminor-vv.

The installer also places a folder of samples and batch file RunSamples.bat on your desktop. To run the samples, just double-click the batch file. Execution may take a few minutes. The binary does not depend on the samples, so you can move or delete the samples without affecting Dminor.

Here is the usage for running Dminor directly on samples. 

    usage: Dminor <target-file> [-verbosity <level>] [-no-type-check]
           [-no-exec | -force-exec] [-run-tests] [-typeful | -inhabited] [-prover-timeout]

        -verbosity <int>: number between 1 (silent) and 5 (default is 2)
        -no-type-check: don't type-check target (default is to type-check)
        -no-exec: don't execute main (default is to run main if well-typed)
        -force-exec: execute main even if target is ill-typed
        -run-tests: run the tests in target (default is not to run them)
        -typeful: Intellipad in #typeful mode
        -inhabited: Intellipad in #inhabited mode
        -prover-timeout <int>: Timeout for Z3 (in milliseconds)
        --help: display this list of options
        -help: display this list of options

Samples

Programs

Every Dminor program is formed by function (and type) definitions contained in a module. For instance the sample file fact.m defines a module named Fact containing one factorial function. The function factorial takes as argument an integer n and returns the integer representing n!. 
module Fact
{

    factorial(n:Integer32) : Integer32
    {
        (n==0)? 1 : n * (factorial(n - 1))
    }
    
    main() : Any
    {
        factorial(10)
    }
}

Types

Dminor is a typed language, however, what makes Dminor really special is that types can contain constrains. For instance given an entity type Person that has a name and an age, we can define the type EligiblePerson that contains only the persons over 17. Then we can state that a marriage can be formed only between eligible persons, and the Dminor type-checker is going to statically verify that this constraint is respected. 
module Constraints
{
    type Person : { Name:Text; Age:Integer32; };
    type EligiblePerson : Person where value.Age > 17;
    type Marriage : { SpouseA: EligiblePerson; SpouseB: EligiblePerson; };
    
    PatChris(): Marriage
    {
      {SpouseA => {Name => "Pat", Age => 24},
       SpouseB => {Name => "Chris", Age => 32}}
    }
    
    /*
   //This does not work
    BillySam(): Marriage
    {
      {SpouseA => {Name => "Billy", Age => 4},
       SpouseB => {Name => "Sam", Age => 5}}
    }
    */
}
If one uncomments the last lines in Constraints.m then Dminor is going to report the following error: 
Type-checking failed
    Function definition BillySam failed to typecheck 408:102. Can't convert {SpouseB
    =>{Name=>"Sam"; Age=>5; }; SpouseA=>{Name=>"Billy"; Age=>4; }; } to type Marriag
    e. Expression can evaluate to {SpouseB=>{Name=>"Sam"; Age=>5; }; SpouseA=>{Name=
    >"Billy"; Age=>4; }; } that does not have type Marriage.

Tagged Unions

module TaggedUnions
{
    type T_tt : {tag: {42}; bar: Integer32;};
    type T_ff : {tag: {43}; foo: Text;};
    type U : T_tt | T_ff;

// this fails to typecheck, because it makes insufficient checks
// Test1(xs:{U*}) : {Text*} { from x in xs select x.foo  }
    
    Test2(xs : {U*}) : {Text*}
    {
        from x in xs
        select ( x.tag==42 ? "Hello" : x.foo )
    }
      
    Test3(xs : {U*}) : {Text*}
    {
        from x in xs
        where (x.tag==43)
        select x.foo
    }
}

Processing DSLs

Tagged unions are very useful for representing the syntax of domain-specific languages. For instance we can represent a the syntax of a simple While language in Dminor, and then build an interpreter that executes While programs. Dminor guarantees that fields are used properly and unexisting fields are never accessed at runtime. 
module SimpleWhileInterpreter
{
    type Operator : Text where
      value=="plus" || value=="minus" ||
      value=="times" //|| value=="div"
      || value=="<=";
    
    type Expression :
    {kind:{"variable"}; name: Text;} |
    {kind:{"integer"}; val: Integer32;} |
    {kind:{"binary app"}; operator: Operator;
      arg1: Expression; arg2: Expression;};
    
    type Statement :
    {kind:{"assignment"}; var: Text; rhs: Expression;} |
    {kind:{"while"}; test:Expression; body:Statement;} |
    {kind:{"if"}; test:Expression; tt:Statement; ff:Statement;} |
    {kind:{"seq"}; s1:Statement; s2:Statement;} |
    {kind:{"skip"};};

    type Store : {{name:Text; val:Integer32;}*};
    
    Var(name:Text) : Expression { {kind=>"variable", name =>name} }
    Int(val : Integer32) : Expression { {kind=>"integer", val=>val} }    
    Plus(arg1 : Expression, arg2 : Expression) : Expression { {kind=>"binary app", operator=>"plus", arg1=>arg1, arg2=>arg2} }
    Minus(arg1 : Expression, arg2 : Expression) : Expression { {kind=>"binary app", operator=>"minus", arg1=>arg1, arg2=>arg2} }
    Times(arg1 : Expression, arg2 : Expression) : Expression { {kind=>"binary app", operator=>"times", arg1=>arg1, arg2=>arg2} }
    Leq(arg1 : Expression, arg2 : Expression) : Expression { {kind=>"binary app", operator=>"<=", arg1=>arg1, arg2=>arg2} }

    Assign(var: Text, rhs: Expression) : Statement { {kind=>"assignment", var => var, rhs => rhs} }
    While(test:Expression,body:Statement) : Statement { {kind=>"while", test=>test, body=>body} }
    If(test:Expression,tt:Statement,ff:Statement) : Statement { {kind=>"if", test=>test, tt=>tt, ff=>ff} }
    Seq(s1 : Statement, s2 : Statement) : Statement { {kind=>"seq", s1=>s1, s2=>s2} }
    Skip() : Statement { {kind=>"skip"} }


    BreakSingleton(xs : Store where value.Count == 1) : Integer32 {
        from x in xs let n = 0 : Integer32 accumulate x.val
    }
    
    // Non-termination is maybe not the best way to signal errors
    Error() : Any where false { Error() }

    Lookup (st:Store, n:Text) : Integer32
    {
        let match = (from x in st where x.name == n select x) in
        (match.Count == 1) ? BreakSingleton(match) : Error()
    }
    
    
    Evaluate(e:Expression, st:Store) : Integer32
    {
       (e.kind == "variable") ? Lookup(st,e.name) : ( 
        (e.kind == "integer")  ? (e.val) : ( 
        (e.kind == "binary app") ? 
         ((e.operator=="plus") ? Evaluate(e.arg1,st) + Evaluate(e.arg2,st) : (
          (e.operator=="minus") ? Evaluate(e.arg1,st) - Evaluate(e.arg2,st) : (
          (e.operator=="times") ? Evaluate(e.arg1,st) * Evaluate(e.arg2,st) : (
          (e.operator=="<=") ?
            (let x1 = Evaluate(e.arg1,st) in
             let x2 = Evaluate(e.arg2,st) in
                (x1 < x2 || x1 == x2)? 1 : 0)
            : "unreachable" //unrecognized operator
         )))
         )
       : (
        "unreachable" //unrecognized expression form
        )))
    }
    
    UpdateStore(x:Text, n:Integer32, st:Store) : Store
    {
        // first remove the previous binding for x
        let st1 = (from y in st where x != y.name select y) in
        // then add a new one
        {{name=>x, val=>n}} ++ st1
    }
    
    Interpret(s:Statement, st:Store) : Store
    {
        (s.kind == "assignment") ? 
            (let rhs = Evaluate(s.rhs, st) in
            UpdateStore(s.var, rhs, st)
        ) : (
            (s.kind == "while") ?
                (let t = Evaluate(s.test, st) in 
                    (t == 0) ? st : (
                        Interpret(Seq(s.body,s), st)
                    )
            ) : (
                (s.kind == "if") ?
                    (let t = Evaluate(s.test, st) in 
                        (t == 0) ? Interpret(s.ff, st) : Interpret(s.tt, st)
                ) : (
                    (s.kind == "seq") ?
                        (let st1 = Interpret(s.s1, st) in 
                            Interpret(s.s2, st1)
                    ) : (
                        st // skip
                    )        
                )
            )
        )
    }
        
    Fact10() : Statement {
        Seq(Assign("f", Int(1)),
        Seq(Assign("i", Int(1)),
        While(Leq(Var("i"), Int(10)),
            Seq(Assign("f", Times(Var("f"),Var("i"))),
            Assign("i", Plus(Var("i"), Int(1)))))))
    }

    main() : Any
    {
        let res = Interpret(Fact10(), {}) in
            Evaluate(Var("f"),res)
    }
}

Queries

Dminor allows one to write LINQ queries that run against collections of values. The type {{Num:Integer32; Flag:Logical;}*} specifies that the expression returns a collection of entities, each of which has a field labeled Num holding a scalar of type Integer32, and a field labeled Flag holding a scalar of type Logical. The expression processes a collection of integers, to yield a collection of entities consisting of the integers n that satisfy the boolean expression {{Num => 4, Flag => true}, {Num => 0, Flag => false}}. 
module Types1
{
    Main() : {{Num:Integer32; Flag:Logical;}*}
    {
        (from n in {5, 4, 0}
        where n < 5
        select {Num =>n, Flag =>(n>0)}):{{Num:Integer32; Flag:Logical;}*}
    }
}

Accumulate

Dminor supports arbitrary comprehensions over collections, which are more general than LINQ queries. The following example illustrates the use of the accumulate construct to enforce that the cost of the servers in a datacenter does not exceed 10000$. 
module Cauldron2 {

    type Pos : Integer32 where value > 0;
    
    type Server : {
    	cost : Pos;
        comp : Computer;
        app : Application;
    } where (value.cost == value.comp.cost + value.app.licenseFee) && value.cost < 2000;

    type Computer : {
        cost : Pos;
    };
    
    type Application : {
        licenseFee : Pos;
    };
    
    type DataCenter : {
    	serv : {Server*} where value.Count > 1 && value.Count < 13;
    } where (from serv in value.serv let s = 0 accumulate s + serv.cost) < 10001;   // sum of all costs

}
Since collections anre unordered accumulate expressions are can be non-deterministic in general. However, if an accumulate expression is used in a refinement Dminor ensures that the expression always evaluates to the same value.

Generating instances of types

Generating Correct System Configurations

inhabited
module SimpleConfigurations {
    
    type GoodPort : Integer32 where value==500 || value==501 || value==502;
    type ServiceName: Text where value=="IIS" || value=="SQL Server";
    type Service: closed {name:ServiceName; port:GoodPort;};
    type Machine: closed {s1:Service; s2:Service;};
    type GoodMachine : Machine where value.s1.port != value.s2.port;   

}
Running Dminor on SimpleConfigurations.m on produces the following output: 
Type GoodPort is inhabited by value 500
Type ServiceName is inhabited by value "IIS"
Type Service is inhabited by value {port=>502; name=>"IIS"; }
Type Machine is inhabited by value {s2=>{port=>500; name=>"SQL Server"; }; s1=>{port=>500; name=>"SQL Server"; }; }
Type GoodMachine is inhabited by value {s2=>{port=>501; name=>"SQL Server"; }; s1=>{port=>500; name=>"IIS"; }; }

Generating Values at Runtime: Enumerating Multiple Correct and Incorrect System Configurations

inhabited
module ElementofIterated {

    type GoodPort : Integer32 where value==500 || value==501 || value==502;
    type ServiceName: Text where value=="IIS" || value=="SQL Server";
    type Service: closed {name:ServiceName; port:GoodPort;};
    type Machine: closed {s1:Service; s2:Service;};
    type GoodMachine : Machine where value.s1.port != value.s2.port;
    type BadMachine : Machine & !GoodMachine;
    
    GenerateAllGoodMachines(avoid : [GoodMachine*]) : [GoodMachine*] {
        let m = (elementof (GoodMachine where !(value contained avoid)))  in
        (m == null) ? ([])
        : (m :: (GenerateAllGoodMachines(m :: avoid)))
    }

    GenerateAllBadMachines(avoid : [BadMachine*]) : [BadMachine*] {
        let m = (elementof (BadMachine where !(value contained avoid)))  in
        (m == null) ? ([])
        : (m :: (GenerateAllBadMachines(m :: avoid)))
    }
    
    main() : Any {
        let g = GenerateAllGoodMachines([]) in
        let b = GenerateAllBadMachines([]) in
        {GoodMachinesCount => g.Length, GoodMachines => g, BadMachinesCount => g.Length, BadMachines => b}
    }
}
Running Dminor on elementof-iterated-lists.m produces the following output: 
Executing (let g=GenerateAllGoodMachines([]) in (let b=GenerateAllBadMachines([]
) in {GoodMachinesCount=>(g.Length); GoodMachines=>g; BadMachinesCount=>(g.Lengt
h); BadMachines=>b; }))...

Result of evaluation:           {GoodMachinesCount=>9; GoodMachines=>[{s2=>{port
=>501; name=>"SQL Server"; }; s1=>{port=>500; name=>"SQL Server"; }; }, {s2=>{po
rt=>502; name=>"IIS"; }; s1=>{port=>500; name=>"SQL Server"; }; }, {s2=>{port=>5
02; name=>"SQL Server"; }; s1=>{port=>500; name=>"SQL Server"; }; }, {s2=>{port=
>501; name=>"SQL Server"; }; s1=>{port=>502; name=>"IIS"; }; }, {s2=>{port=>500;
 name=>"IIS"; }; s1=>{port=>501; name=>"IIS"; }; }, {s2=>{port=>501; name=>"IIS"
; }; s1=>{port=>500; name=>"IIS"; }; }, {s2=>{port=>500; name=>"IIS"; }; s1=>{po
rt=>502; name=>"SQL Server"; }; }, {s2=>{port=>501; name=>"SQL Server"; }; s1=>{
port=>500; name=>"IIS"; }; }, {s2=>{port=>501; name=>"SQL Server"; }; s1=>{port=
>502; name=>"SQL Server"; }; }]; BadMachinesCount=>9; BadMachines=>[{s2=>{port=>
501; name=>"IIS"; }; s1=>{port=>501; name=>"SQL Server"; }; }, {s2=>{port=>500;
name=>"SQL Server"; }; s1=>{port=>500; name=>"IIS"; }; }, {s2=>{port=>501; name=
>"SQL Server"; }; s1=>{port=>501; name=>"SQL Server"; }; }, {s2=>{port=>501; nam
e=>"SQL Server"; }; s1=>{port=>501; name=>"IIS"; }; }, {s2=>{port=>502; name=>"S
QL Server"; }; s1=>{port=>502; name=>"SQL Server"; }; }, {s2=>{port=>500; name=>
"SQL Server"; }; s1=>{port=>500; name=>"SQL Server"; }; }, {s2=>{port=>500; name
=>"IIS"; }; s1=>{port=>500; name=>"IIS"; }; }, {s2=>{port=>501; name=>"IIS"; };
s1=>{port=>501; name=>"IIS"; }; }, {s2=>{port=>502; name=>"SQL Server"; }; s1=>{
port=>502; name=>"IIS"; }; }]; }

Cauldron

inhabited
module Cauldron {

    type Pos : Integer32 where value > 0;
    
    type Server : {
    	cost : Pos;
        comp : Computer;
        app : Application;
    } where (value.cost == value.comp.cost + value.app.licenseFee) && (value.cost < 2000) &&
            (value == {cost => value.cost, comp => value.comp, app => value.app});

    type Computer : {
        cost : Pos;
    } where value == {cost => value.cost};
    
    type Application : {
        licenseFee : Pos;
    } where value == {licenseFee => value.licenseFee};
    
    type DataCenter : {
    	serv : [Server#6];
        managers : [Server#2];
    } where ((value.managers[0] contained value.serv) && (value.managers[1] contained value.serv) && (value.managers[0] != value.managers[1]));

}
Running Dminor on Cauldron.m produces the following output: 
Type Pos is inhabited by value 1
Type Server is inhabited by value {cost=>1727; comp=>{cost=>1726; }; app=>{licen
seFee=>1; }; }
Type Computer is inhabited by value {cost=>1; }
Type Application is inhabited by value {licenseFee=>1; }
Type DataCenter is inhabited by value {serv=>[{cost=>1202; comp=>{cost=>803; };
app=>{licenseFee=>399; }; }, {cost=>1203; comp=>{cost=>803; }; app=>{licenseFee=
>400; }; }, {cost=>1203; comp=>{cost=>803; }; app=>{licenseFee=>400; }; }, {cost
=>802; comp=>{cost=>402; }; app=>{licenseFee=>400; }; }, {cost=>1203; comp=>{cos
t=>803; }; app=>{licenseFee=>400; }; }, {cost=>1202; comp=>{cost=>803; }; app=>{
licenseFee=>399; }; }]; managers=>[{cost=>1202; comp=>{cost=>803; }; app=>{licen
seFee=>399; }; }, {cost=>1203; comp=>{cost=>803; }; app=>{licenseFee=>400; }; }]
; licenseFee=>31; cost=>33; app=>32; }