View Source cure_refinement_types (cure v0.7.0)

Refinement Types with SMT Verification

This module implements refinement types - types augmented with logical predicates that are verified at compile-time using the Z3 SMT solver.

Refinement Types

A refinement type refines a base type with a logical predicate:

type Positive = Int when x > 0
type NonZero = Int when x != 0
type Percentage = Int when x >= 0 and x =< 100

Subtyping

Refinement subtyping is verified using SMT:

Positive <: NonZero   (proven by Z3: x > 0 => x /= 0)

Features

  • Extract constraints from refinement type definitions
  • Verify subtyping relationships via SMT
  • Check function preconditions and postconditions
  • Propagate constraints through function calls
  • Generate counterexamples for constraint violations

Summary

Types

expr()
location()
refinement_type()
type_expr()

Functions

base_type/1
check_constraint/3
check_subtype(Type1, Type2, Env)
create_refinement_type(BaseType, Var, Predicate)
extract_constraint/1
format_refinement_error/1
generate_counterexample/2
is_refinement_type/1
propagate_constraints(Expr, Env, ConstraintMap)
refinement_predicate/1
strengthen_type(BaseType, AdditionalConstraint, Var)
verify_postcondition(ReturnExpr, ReturnType, Env, Location)
verify_precondition(ArgExpr, ParamType, Env, Location)
verify_subtype_smt/3
weaken_type/2

Types

expr()

-type expr() ::
          #literal_expr{value :: term(), location :: term()} |
          #identifier_expr{name :: term(), location :: term()} |
          #function_call_expr{function :: term(), args :: term(), location :: term()} |
          #match_expr{expr :: term(), patterns :: term(), location :: term()} |
          #let_expr{bindings :: term(), body :: term(), location :: term()} |
          #binary_op_expr{op :: term(), left :: term(), right :: term(), location :: term()} |
          #unary_op_expr{op :: term(), operand :: term(), location :: term()} |
          #list_expr{elements :: term(), location :: term()} |
          #vector_expr{elements :: term(), location :: term()} |
          #tuple_expr{elements :: term(), location :: term()} |
          #record_expr{name :: term(), fields :: term(), location :: term()} |
          #field_access_expr{record :: term(), field :: term(), location :: term()} |
          #record_update_expr{name :: term(), base :: term(), fields :: term(), location :: term()} |
          #lambda_expr{params :: term(), body :: term(), location :: term()} |
          #forall_expr{variables :: term(), body :: term(), location :: term()} |
          #exists_expr{variables :: term(), body :: term(), location :: term()} |
          #fsm_spawn_expr{fsm_name :: term(),
                          init_args :: term(),
                          init_state :: term(),
                          location :: term()} |
          #fsm_send_expr{target :: term(), message :: term(), location :: term()} |
          #fsm_receive_expr{patterns :: term(), timeout :: term(), location :: term()} |
          #fsm_state_expr{location :: term()} |
          #melquiades_send_expr{message :: term(), target :: term(), location :: term()} |
          #qualified_call_expr{trait_name :: term(),
                               type_args :: term(),
                               method_name :: term(),
                               receiver :: term(),
                               args :: term(),
                               location :: term()}.

location()

-type location() :: #location{line :: term(), column :: term(), file :: term()}.

refinement_type()

-type refinement_type() ::
          #refinement_type{base_type :: term(),
                           variable :: atom(),
                           predicate :: term(),
                           location :: term()}.

type_expr()

-type type_expr() ::
          #primitive_type{name :: term(), location :: term()} |
          #dependent_type{name :: term(),
                          type_params :: term(),
                          value_params :: term(),
                          location :: term()} |
          #function_type{params :: term(), return_type :: term(), location :: term()} |
          #union_type{types :: term(), location :: term()} |
          #list_type{element_type :: term(), length :: term(), location :: term()} |
          #tuple_type{element_types :: term(), location :: term()} |
          #fsm_type{name :: term(), states :: term(), message_types :: term(), location :: term()} |
          #process_type{fsm_type :: term(), current_state :: term(), location :: term()} |
          #genserver_ref_type{variant :: term(), location :: term()}.

Functions

base_type/1

-spec base_type(refinement_type()) -> type_expr().

check_constraint/3

-spec check_constraint(expr(), refinement_type(), map()) -> {ok, boolean()} | {error, term()}.

check_subtype(Type1, Type2, Env)

-spec check_subtype(term(), term(), map()) -> {ok, boolean()} | {error, term()}.

create_refinement_type(BaseType, Var, Predicate)

-spec create_refinement_type(type_expr(), atom(), expr()) -> refinement_type().

extract_constraint/1

-spec extract_constraint(refinement_type()) -> {ok, expr()} | {error, term()}.

format_refinement_error/1

-spec format_refinement_error(term()) -> binary().

generate_counterexample/2

-spec generate_counterexample(expr(), refinement_type()) -> {ok, map()} | {error, term()}.

is_refinement_type/1

-spec is_refinement_type(term()) -> boolean().

propagate_constraints(Expr, Env, ConstraintMap)

-spec propagate_constraints(expr(), map(), map()) -> map().

refinement_predicate/1

-spec refinement_predicate(refinement_type()) -> expr().

strengthen_type(BaseType, AdditionalConstraint, Var)

-spec strengthen_type(type_expr(), expr(), atom()) -> refinement_type().

verify_postcondition(ReturnExpr, ReturnType, Env, Location)

-spec verify_postcondition(expr(), refinement_type(), map(), location()) -> ok | {error, term()}.

verify_precondition(ArgExpr, ParamType, Env, Location)

-spec verify_precondition(expr(), refinement_type(), map(), location()) -> ok | {error, term()}.

verify_subtype_smt/3

-spec verify_subtype_smt(refinement_type(), refinement_type(), map()) ->
                            {ok, boolean()} | {error, term()}.

weaken_type/2

-spec weaken_type(refinement_type(), [atom()]) -> type_expr().