1
$\begingroup$

While most main stream programming languages allow for user defined types that can have the following properties:

  • associative
  • commutative
  • distributive

the only way I know of that this can be shown to be correct is to use models to prove it correct for each user defined type.

As an example the language F* (FStar) includes the model rules in the programming language. Here is an example rule for association for one type:

assume ConcatAssocR: forall a b c.{:pattern (Concat (Concat a b) c)}  
  Concat (Concat a b) c = Concat a (Concat b c)

Note: I don't use F* but am considering learning it.

Since most programming is done without using models, to prove the program correct are there other ways that proving these rules hold for user defined type can be done for a program?

Further expanding the idea, are there any attacks that exploit the lack of proving these properties?
(I know this is a security question, but some of those people hang out here.)

$\endgroup$
  • 1
    $\begingroup$ I'm confused as what you are asking: you can always test that a property like the above holds, e.g. using a framework like QuickCheck. In general though, proving properties about code requires a) an external (language-specific) tool like Frama-C or b) an external verification based on the semantics of your language (e.g. Compcert). As for security, it's pretty clear that most bugs may lead to security problems. $\endgroup$ – cody Jul 2 '14 at 14:29
  • $\begingroup$ @cody Your comment gave reasonable answers, so what is confusing? $\endgroup$ – Guy Coder Jul 2 '14 at 15:10
  • 1
    $\begingroup$ @cody I have used tools like QuickCheck, but don't consider them as a means of proving, but as a means of providing evidence. I have not used Frama-C, but from a quick read on it, it appears to be in the same category as the model example. I am not sure I understand if Compcert is an answer because as I understand it, it verifies the compiler and not the final program. Thanks. $\endgroup$ – Guy Coder Jul 2 '14 at 15:10
  • $\begingroup$ Well it doesn't even make sense to prove a property about a programing language if you don't have a mathematical model of it's operational semantics. Compcert does exactly this for C (and it's hard to do!), before proving that the compiler respects these semantics. Alternatively, you can have a language that is both a specification language and a proof language bundled together, as in the case of $F^*$ and express (and maybe prove) the properties directly in the language itself. Frama-C is closer to the latter. $\endgroup$ – cody Jul 2 '14 at 17:36
  • $\begingroup$ @cody I made a correction in the question. "Since most programming is done without using models to prove the program correct, are there other ways that proving these rules hold for user defined type can be done for a program?" is "Since most programming is done without using models, to prove the program correct are there other ways that proving these rules hold for user defined type can be done for a program?" notice the comma moved which changed the meaning. My mistake. $\endgroup$ – Guy Coder Jul 2 '14 at 18:28

Your Answer

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

Browse other questions tagged or ask your own question.