Hi Theoretical Computer Science Stack Exchange,
I have been wondering if there are programming languages where one can have constraints on values variables can have? Have such approach been used in programming language research? I'm aware of testing, static analysis, model checking, and formal verification and was thinking if constrains, like in optimization, would provide another approach for building better quality software.
- (Example 1) Suppose we want to define a data structure for circle, using doubles. Since unsigned double does not exist in C, one could have (modified C syntax below)
struct circle {
double x;;
double y;;
double radius; radius >= 0;
}
As you can see, the constraints are placed between ';' symbols. The idea is to ensure correctness/validity of the values of a circle when constraint checking is on.
- (Example 2) Suppose we want to implement an closed interval in $double$ with a point in it. Something like
struct closed_interval_and_point {
double min;;
double max;;
double point; min <= point && point <= max;
}
This example motivates unlock and lock features for constraint checking. To modify interval a point might lie outside the interval for a moment. Something like
struct closed_interval_and_point var = {.min = 0.0f, .max = 1.0f, .point = 0.5f};;
unlock var.point;; // unlock constraint checking for var.point
var.min = 2.0f;;
var.max = 4.0f;;
var.point = 3.0f;;
lock var.point;; // lock constraint checking for var.point
might be used to enable modification of structure. Constraint checking would be off after unlock and done after lock command and after it. (One could also replace unlock by off and lock by on, perhaps those keywords would be better, here I just describe the idea).
(Idea 1) Constraint checking could be implemented using valgrind style environment, where each modification to memory address can be tracked. Every time a value in memory changes, the language would check the constraints related to the value, in case constraint checking is locked.
(Idea 2) The idea of extending C with constraints is that once one has run program with multiple inputs with no constraint violations, one could extract a normal C program which does not have constraint checks, but which has been "validated" in the constrained environment.
(Question 1) Has this approach been researched in academia or industry? If so, what is the keyword for finding this kind of languages/extensions? If not, I think this approach could be fundamentally different(?) than testing, debugging, static analysis, model checking and formal verification. Of course, I have no data to show that this constraint approach would be successful/useful.
(Question 2) I know my examples are incomplete in detail. I believe that a complete discussion of the subject is inappropriate in this forum. Where could I discuss this idea further?
Best Regards,
Tomi Pannila
Errata : Valgrind -> GDB watchpoint
