0
$\begingroup$

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.

  1. (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.

  1. (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).

  1. (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.

  2. (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.

  3. (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.

  4. (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

$\endgroup$
4
  • $\begingroup$ Don't dependent types, refinement types, liquid types do what you have in mind? See e.g. Liquid Haskell. $\endgroup$ Apr 21 at 18:40
  • $\begingroup$ Yes, I think a relevant keyword here is "refinement types". There is a very short Wikipedia entry about them, searching Google should give you more detailed results. $\endgroup$ Apr 22 at 8:05
  • $\begingroup$ Hi @Martin_Berger and Damiano_Mazza, Both "refinement type" and "dependent type" seem to be correct. Than you for referring to Liquid Haskell, RefinedC seemed also interesting. I was looking for a mainstream imperative language embedded with easy to use constraints on values. I see there is active research on the subject "refinement types", and implementations related to it, so I hope that in future we will see refinement types motivated prototypes brought to at least C structs, C++ classes and Java classes for structural soundness checks, not full formal verification. $\endgroup$ Apr 23 at 14:09
  • $\begingroup$ Since version 8.0, C# has non-nullable reference types. This is incredibly useful in my day job. Does this fit the bill? docs.microsoft.com/en-us/dotnet/csharp/nullable-references $\endgroup$ May 3 at 6:33

0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.