6 ms·

That's why you implement it in Ada 2012 w/ SPARK 2014. You can encode the verification conditions as contracts. All the basic ones should be proven automaticall

That's why you implement it in Ada 2012 w/ SPARK 2014. You can encode the verification conditions as contracts. All the basic ones should be proven automatically. Those that aren't can be turned into runtime checks. https://en.wikipedia.org/wiki/SPARK_(programming_language) https://en.wikipedia.org/wiki/SPARK_(programming_language) http://www.electronicdesign.com/industrial/rust-and-spark-software-reliability-everyone http://www.electronicdesign.com/industrial/rust-and-spark-so... Here's an example of combining Event-B with SPARK to split overall verification between tools with each handling what they're good at: https://pdfs.semanticscholar.org/481c/d4d2409115429f4b824f370eb08fa338d67a.pdf https://pdfs.semanticscholar.org/481c/d4d2409115429f4b824f37...

unboxed_type 9y ago
How well Ada/SPARK suits distributed control algorithms I wonder? As far as I understand contracts are good enough for sequential code, but not well suited for parallel/distributed computation? Runtime checks are good as to prevent something from happening, but they are not able to guarantee the absence of an error in the first place, right?
- oconnore 9y ago
  Huh? The whole point of distributed algorithms is that a set of local algorithms create a global behavior. I received this message so I send that message, etc. The SPARK contracts you write would check that local behavior, and the TLA+ would check that that local behavior results in some global behavior.
  - unboxed_type 9y ago
    Well, TLA+ checks your 'contract' by traversing states of your model explicitly which takes a lot of time usually while in ADA we have to deduce feasibility of a contract at compile time. Checking a property of a distributed system at compile time is generally a hard problem, so I expect that ADA`s ability to do this should be rather limited.
    - oconnore 9y ago
      You wouldn't write an Ada contract describing the full system, you would write one describing the local behavior you just described in your TLA+ model. The model ensures that the emergent behavior of the system is correct, and the local contract ensures that the local behavior of the various actors is correct -- and therefore results in that emergent behavior. Combined, that's a fairly solid argument that your system does what you intended. If you had to implement the full proof in Ada, there would be no point to doing the TLA+ work.
      - nickpsecurity 9y ago
        "You wouldn't write an Ada contract describing the full system, you would write one describing the local behavior you just described in your TLA+ model. The model ensures that the emergent behavior of the system is correct, " This is how I was seeing it happen, too.
      - unboxed_type 9y ago
        Oh, now I see your point. Checking a TLA+ model of an algorithm and then implementing each actor in Ada reinforcing it with pre/post conditions perfectly makes sense. Its just a little out of scope of the current thread, because the author of parent message was talking about using pure Ada/SPARK, without help of TLA+ (As I understand it in the first place), so my comment about using contracts was in that context.
        nickpsecurity 9y ago
        No, I meant implementation in SPARK. The specs were already done in TLA+ in the OP's model. There's also implied porting between two notations.
- pjmlp 9y ago
  A good book about is "Building High Integrity Applications with SPARK". http://www.cambridge.org/us/academic/subjects/computer-science/programming-languages-and-applied-logic/building-high-integrity-applications-spark#YwR5KJ9q84ZfjiLy.97 http://www.cambridge.org/us/academic/subjects/computer-scien... Ada/SPARK has parallel computations defined at language level, known as tasks.
  - unboxed_type 9y ago
    Thanks for the reference.
pron 9y ago
No need to use Ada, though. Similarly powerful options exist for Java and C. The code-level specification language is JML (Java) or ACSL (C), and there are many verification tools, from SMT solvers, through proof assistant obligations, to concolic or randomized test generation. Nevertheless, you're never certain doing that, either, as you don't formally tie the code-level specification to the high-level specification. That's OK, though, because end-to-end specification is neither required for most software nor currently possible for anything other than small, relatively simple software.
- nickpsecurity 9y ago
  They exist but SPARK's were much better on automated proving. It was due to SPARK being a simpler language designed explicitly for verification.
  - pron 9y ago
    Right, but this is because SPARK is (intentionally) limited. For example, AFAIK, you can't dynamically allocate memory in SPARK. If you write Java code that is as simple as SPARK code, it would also be automatically verified (after all, the solvers are the same). Java also has automated verification that does separation logic, and works well with dynamic memory (Facebook's Infer). Languages that truly admit full automatic verification (and are also limited) -- including rich global correctness properties -- are synchronous languages for safety-critical realtime, like SCADE. BTW, SPARK contracts are not so rich. There are many useful properties that you can't express.
    - nickpsecurity 9y ago
      "If you write Java code that is as simple as SPARK code, it would also be automatically verified (after all, the solvers are the same)." Java has a different model than SPARK. Especially if you're considering verifying it against the JVM or against assembly. SPARK will probably have an advantage given the papers I've read on JML work. Far as it's overall tooling, I'm aware it has a bunch for proofs and testing as it's one of three I mention to look for in supposedly, high-assurance projects (others being C subsets & Ada/SPARK). Infer is new to me, though, so thanks for mentioning it. "BTW, SPARK contracts are not so rich. There are many useful properties that you can't express." Hence, work like E-SPARK that combines Event-B and SPARK. Another I saw uses SPARK, TLA+, and UPAAL for timing analysis on stuff already analyzed at component level. Best to mix and match. DeepSpec with CertiKOS is probably state of the art in that far as popular stuff goes. My Brute Force Assurance concept will do it differently if I implement it where I mix automated analysis and testing tools for code generated in C, Java, and SPARK where each's toolchain catches something the others miss. Semantic mismatches could be a problem but I'm hoping something could come out of it.

unboxed_type 9y ago

How well Ada/SPARK suits distributed control algorithms I wonder? As far as I understand contracts are good enough for sequential code, but not well suited for parallel/distributed computation? Runtime checks are good as to prevent something from happening, but they are not able to guarantee the absence of an error in the first place, right?

oconnore 9y ago
Huh? The whole point of distributed algorithms is that a set of local algorithms create a global behavior. I received this message so I send that message, etc. The SPARK contracts you write would check that local behavior, and the TLA+ would check that that local behavior results in some global behavior.
- unboxed_type 9y ago
  Well, TLA+ checks your 'contract' by traversing states of your model explicitly which takes a lot of time usually while in ADA we have to deduce feasibility of a contract at compile time. Checking a property of a distributed system at compile time is generally a hard problem, so I expect that ADA`s ability to do this should be rather limited.
  - oconnore 9y ago
    You wouldn't write an Ada contract describing the full system, you would write one describing the local behavior you just described in your TLA+ model. The model ensures that the emergent behavior of the system is correct, and the local contract ensures that the local behavior of the various actors is correct -- and therefore results in that emergent behavior. Combined, that's a fairly solid argument that your system does what you intended. If you had to implement the full proof in Ada, there would be no point to doing the TLA+ work.
    - nickpsecurity 9y ago
      "You wouldn't write an Ada contract describing the full system, you would write one describing the local behavior you just described in your TLA+ model. The model ensures that the emergent behavior of the system is correct, " This is how I was seeing it happen, too.
    - unboxed_type 9y ago
      Oh, now I see your point. Checking a TLA+ model of an algorithm and then implementing each actor in Ada reinforcing it with pre/post conditions perfectly makes sense. Its just a little out of scope of the current thread, because the author of parent message was talking about using pure Ada/SPARK, without help of TLA+ (As I understand it in the first place), so my comment about using contracts was in that context.
      - nickpsecurity 9y ago
        No, I meant implementation in SPARK. The specs were already done in TLA+ in the OP's model. There's also implied porting between two notations.
pjmlp 9y ago
A good book about is "Building High Integrity Applications with SPARK". http://www.cambridge.org/us/academic/subjects/computer-science/programming-languages-and-applied-logic/building-high-integrity-applications-spark#YwR5KJ9q84ZfjiLy.97 http://www.cambridge.org/us/academic/subjects/computer-scien... Ada/SPARK has parallel computations defined at language level, known as tasks.
- unboxed_type 9y ago
  Thanks for the reference.

pron 9y ago

No need to use Ada, though. Similarly powerful options exist for Java and C. The code-level specification language is JML (Java) or ACSL (C), and there are many verification tools, from SMT solvers, through proof assistant obligations, to concolic or randomized test generation. Nevertheless, you're never certain doing that, either, as you don't formally tie the code-level specification to the high-level specification. That's OK, though, because end-to-end specification is neither required for most software nor currently possible for anything other than small, relatively simple software.

nickpsecurity 9y ago
They exist but SPARK's were much better on automated proving. It was due to SPARK being a simpler language designed explicitly for verification.
- pron 9y ago
  Right, but this is because SPARK is (intentionally) limited. For example, AFAIK, you can't dynamically allocate memory in SPARK. If you write Java code that is as simple as SPARK code, it would also be automatically verified (after all, the solvers are the same). Java also has automated verification that does separation logic, and works well with dynamic memory (Facebook's Infer). Languages that truly admit full automatic verification (and are also limited) -- including rich global correctness properties -- are synchronous languages for safety-critical realtime, like SCADE. BTW, SPARK contracts are not so rich. There are many useful properties that you can't express.
  - nickpsecurity 9y ago
    "If you write Java code that is as simple as SPARK code, it would also be automatically verified (after all, the solvers are the same)." Java has a different model than SPARK. Especially if you're considering verifying it against the JVM or against assembly. SPARK will probably have an advantage given the papers I've read on JML work. Far as it's overall tooling, I'm aware it has a bunch for proofs and testing as it's one of three I mention to look for in supposedly, high-assurance projects (others being C subsets & Ada/SPARK). Infer is new to me, though, so thanks for mentioning it. "BTW, SPARK contracts are not so rich. There are many useful properties that you can't express." Hence, work like E-SPARK that combines Event-B and SPARK. Another I saw uses SPARK, TLA+, and UPAAL for timing analysis on stuff already analyzed at component level. Best to mix and match. DeepSpec with CertiKOS is probably state of the art in that far as popular stuff goes. My Brute Force Assurance concept will do it differently if I implement it where I mix automated analysis and testing tools for code generated in C, Java, and SPARK where each's toolchain catches something the others miss. Semantic mismatches could be a problem but I'm hoping something could come out of it.