1. A method for testing at least one type of declarative program, including: receiving an expression of a programming construct of a declarative program generated according to a declarative programming model having a type system supporting refinement types combined with type membership evaluation; attempting to synthesize a type for the expression; and checking whether the expression in a given context has the type.