Contract Based Programming in Ada 2012
CC Attribution 2.0 Belgium:
You are free to use, adapt and copy, distribute and transmit the work or content in adapted or unchanged form for any legal purpose as long as the work is attributed to the author in the manner specified by the author or licensor.
Andersen, Jacob Sparre
A tutorial on how to use the Ada 2012 features for specifying detailed, checked contracts for types and subprograms - "classes, functions, and methods" if you aren't an Ada programmer already. Contracts document constraints on how types and subprograms behave, but unlike comments they are checked - either by when the program is compiled or on-the-fly as the program is running. Ada 2012 contract aspects will be presented together with a set of guidelines for using contract aspects consistently. The tutorial will conclude with a live test of the guidelines on some example source text.
 So I'll put on this as a tutorial. We'll start out tomorrow as a common presentation. And I have an example. I did it. It was going to give me an example. So I didn't make up an example. I healed the task, but I didn't have to work on two wheels. But I'm going to talk about how to use. I think you should use the aspects of implementation programming in the media stuff. So just so I sort of know, how many of you have not programmed in it at all? OK. That's good to know. If you happen to hear either some peers talk this morning or the previous one, OK, so how do you think what you said about it? I don't. Me, I'm independent and sometimes I'm not really doing software development stuff, but also interesting thing like inspecting mobile platforms and starting up with new games, starting finance. And well, since we have all heard about that much about data before, I'll just say some of the reasons why we should be using data. I need to design on this data of seeing programming as a human security about reliability and about maintenance. Contracts in data that mostly are reliability and maintenance as the contract is form of documentation, which has added benefit of actually being checked by the client the entire time or other time, so it's really reliability and way. That's a very short story about ADEN. Then I have a presentation of ADEN in a simple slide, which is not enough to learn about ADEN, but you can get an idea about it. Is procedural programming language is a form of public-dialogical programming? You're not forced to use public-dialogical programming, but you can do it. There's what you call multiple programming. You can separate your project packages, file packages. You have individual standards on some programs. There's generics, which is an alternative to public-dialogical programming that's what generalizes your solutions. One thing that I like very much, and it's also very relevant about time management, is the separation of declarations of top programs and packages and the actual implementation of them. First, you specify the interface, then separate from that, we write back the documentation just to make sure you're doing the right thing. We have to repeat the basics of the specification. Then, as the current speaker, we will have programming facilities to go into the language, not just the hospital, not just ad-on languages, but actually as a part of the language specification. Then, in 1997, I have something to think of as a name, rather than just by what value status the hospital's running for. It comes at a time like 40 classes in our technical program, and for simple times, like various people do at home, on other times. The most recent standard was published, more or less, and they did not publish in 1990. What is it? In 1990, first grade, 50% of 2012, the initial course in the human history. But then, the regulations are on the 12 standard, only one in the series. Some of this, which is new, exactly about the basic programming, that's the ability to prepare pre and first conditions for sub-programs, which is, as a minimum, the long-term runtime checks and the state of parameters for sub-programs before and after a phone. Then there's time variance and sub-time predicates, which are the kinds of constraints which should be consistent for all updates and there's time, time at all times. The differences between these three is the time variance, like checks and private types, where you have in-vay implementation details, exactly which components exist at this time, where predicates that for technically for sub-types, but for types where you have visibility in the terminals, and they act more as constraints and different dynamic constraints, that is related to how easy it is basically to do a compile time analysis. I have an example later on where you'll see that with compiler, actually already with an app, TPO 2013 edition, and a patch, is that compile time programming error, in a case where it's done in some time predicates. Hopefully in the future we'll have more of the smart tool facilities migrating into the compiler so we'll have messages when you compile. Well, your program's available in the country running, but this line, the policy, you're not fulfilling some condition. But we're not quite there yet. So you'll go back to Paris to work on it soon. If you do not the thing that people will say, oh, the compiler is just a wall now. Well, yes, I have... So now you still have to run various tools, besides the client, yes, in time time. But besides all this new and fancy stuff, you have the data programmers, makers, and the input tool. But also, we have the name, primitive types. If you have specific type, even if you have another type with exactly the same values, you can't just copy between objects at the same time. You have to make explicit conversions. You have currently the passing directions on your subprogram. So you have to tell explicitly if an argument for a subprogram is apparently going in, apparently they're going out. Like, one that's going both ways, and then out after some time in the page. And then we have the rate checks on the rates. So you don't accidentally call on the vercos in address, outside, and array. And then we have sub-times, which is basically having an existing type and then make a subset of it for the ranges. And then there's some cases where you have static checks, like that a case statement covers all the possible values of document for case statements. You get a complaint and an email error because of how many of these are all the possible values. Some of this is higher time checks. Some of this is one-time checks. But it all helps. Catching errors earlier and later. And there is the better. I've used contracts on a medium-sized product, but it's the last year and a half. And I must admit that even though we're using them, I'm not sure we've actually called any errors directly by the pilot saying he did something wrong. Must admit that. But it could be because we have good programmers. It could also be because they're not assigning the final contracts that much against us. So now I'll start going through each kind of contract elements. We have in data 2012 come up with some comments and a small example. We'll start with a pre-condition and from the rationale for the data result it's an application under form. All of us ensure that something is in order before you form the sub-program. And it's a guarantee that if you're going to implement the sub-program like this, this is true once you're formed. And I just came up with an example. Eating data from the pilot, but haven't actually put any of these contract aspects much of the standard libraries. So I decided to just take some examples from the take my own API data. So we say we want to put a spring to a context file. Well, we better make sure the file is open first. So this is one example you can put in on a pre-condition. Still, in this case, we could of course have a race condition that, well, once we call it, it's okay, but there always is marked file system or makes some strange things. Meanwhile, so the abrasion can still fail in these cases. But it's a nice minimal requirement in the case. Similarly, in your first conditions, you're staying half done, talking to us when you're calling a sub-program. That's an obligation and the incumbent of the sub-program to make sure that this is true once the sub-program returns. And it's a promise, a lot of hands to the call, and that this is how the world will be afterwards. And I decided then, okay, let's take the line and we can take the IO API. And data has, depending on your view, an eyes or an eye, an eye, and a house of feature, a keeping track of line numbers and the file when you're writing through it, a reading from it. So actually, we can say that after you've done the line, the line number has been implemented by one. So that's an example of a post-condition. Here, I reference the value of the line number before calling through this item node. Yeah, I'm not going to teach you the details of the syntax of data in this talk. That would take more than an hour. So there are lots of good references for that. That was three post-conditions then. Time in arrays. This is an example I've adapted from the 2012 rationale. Imagine you want to have, we've got 12 reactions. We want to have the time in, the time in through a percentage function of the unit. That was the mathematician one. The function is earlier. We can start by just saying, well, we do it in random vector, and we'll have four names. Yeah. But then, flow then, you can see anywhere, then with the limit times minus one to one, and we get it into this box here. But we don't want it turned off here. We can do that with time in arrays that the distance from the cargo shouldn't go beyond one. So now we have the type here for managing the response of the unit base. Of course, there could be any type of conditions here. But the point is that this is something that the compiler now is obliged to do to objects of type this point. But it always has to be true. Yeah. You go back here. That's good. Very good. A good point derived from one that was just an arbitrary point where you'd say, okay, it can be anywhere as far as building point type for the sense. And then we use this as a subtype, the subtype constraint. Then the kind of variance that's dynamic in subtype predicates. That's kind of constraints in sub-setting subtypes. If you look at an example here, a prime, it's an integer. It can't be less than two. And you can't have any factors to the number which are different from one and the number itself. Which if we look at the here, we're saying that prime line was n to zero. That happens for some n from two up to prime minus one. Then it's not the R dynamic predicate. It's not the truth. So now we have a subtype of integers which is only the prime. Unfortunately, you can't do fancy stuff by looping over a subtype of the dynamic predicate. You can do that with the standard predicate. But you can have these made. Now you can just, the lazy test now for which integers are prime is to just loop over all the integers and see if you can, it's in the subtype prime. Because it's not necessarily computationally efficient, but that's a different matter. This is an example of an actual project where there was a decision somewhere that this organization Ui could not be longer than 256 characters. And to avoid that we accidentally in our program tried to put a larger string, longer strings into our database, we made this subtype where we put in a dynamic predicate and the length of these strings. In older versions of A8, you could do something similar by creating a bounded string which would have length of 256 characters. But all the work during that, this is much easier. And then, I said before it was dynamic, subtype predicate. Subtype predicate, they are more limited in what, basically it's the same, but it's more limited with expressions you're allowed to use. You can do anything where your subtype is in a statically defined sense or part of an otherwise static expression. There's some operations you can do at least. It's not all. But this is one of the cases, look it up in the reference manual when you get to it. And I was in Mauritius recently working for a small data company there. So I decided, well, we'll make a nice example of the summer burn from November to April. How was the end of the week? That's a different story. So now we have a type of month, just made a short business, an example of an operation time to data. And then I make a subtype where I say, okay, the summer month, that's in November to December and then from January to April. And then I declare an update. And then I accidentally switch back to northern chemistry mode and say, well, July is the summer month, but trying that with a compiler, you get the warning group that doesn't work. You get a failure because July is not the summer subtype. There's a similar example in the government program, no, but it's by grid fire and Englishman that is clearly not used to the concept that the summer could go from November to April. So it does, with a window from December to January, the very exact effect is the same. And then I talk about coverage change. Here I have a, well, not very nice example of a case statement. Level is, if there's the level of some of the logic messages, which is the very true level, and then we say the different operations which we're to send the messages depending on the level. It's split out to the case-thens statement, but what would happen if I accidentally forgot to put in the alert level? What would happen would be that the island would say that I'm not telling all the possible values of the tidal level and it would stop from crying in my program. I'd have to go P.A. and do something. It's not directly contract, but it's a very useful static implementation check. And it relates to the subtype of this value you put in. So that was the quicker overview of contracts in April 2012. Now, say I look like this senior, I've got everything included. Yeah. Okay. I've got my best to put some guidelines together to get a consistent use of contract-based programming in AIDA. When I started, I just put things in and write them on a sort of.NET file. We can put something in here. It's better if you do it consistently across the application or your library. And the place I like to start when I'm programming, that's with the types. So, make sure that you make good detailed declaration of the type and its constraints. You declare type or subtype depending on the requirements of compatibility with other types. You want to be fast-directed or if it should be really unique type that you should expect to be back and forth. You can put appropriate constraints in your values. I had the example where the point squared was the constraint that the 30-point coordinate shouldn't be less than minus 1 at the end point as an example. And then you can add extra examples, extra constraints, any displeasure as predicates or varies in the type. But I think you'll see that in many cases you don't really need that. This is enough in the kind of other contracts for a time. So, I go back to my introduced in my primary example. We start off with this, crime-plated introduced. And I decided here that, well, it's really an integer. It's not that special. So it's just a subtype of integer. If I thought it was really something special, I would say crime type crime is new integer and it would be a new type just having to be derived from integer time. And then there's this about crime is being largely done one after the range constraint done. And crime is a nice approach. That's not enough. We also need to keep track of the only factors that's one of the crimes itself. So, an example, Native Country, these items, I have to say so, I have used it in real-time. I did use Spark once to validate applications of my crimes. And it found an error. I hadn't found it by testing. I was impatient. If I had to let it try to run to the end, it would have faded around there because there was some mismatch running over the edge of the number of that integer in the process. It took some time to figure out that it was that that Spark was telling you it was wrong. It's definitely useful and it's useful in cases where you have the patients to find it by testing. I know also that the Spark people are being involved in testing a cryptographic hash function where there's a Spark in the reference implementation. If you give it 2 to the 64, 5 long data sets to hash, it gets the wrong value. And nobody apparently have tested that. So the bug is still there, though it has been reported. But then, back to the main story, now we have declared our times. The next step, that's the sub-programs which are going to operate in these times. And not going to inter-detail on the sub-programs themselves. But when we have no which one we need, make sure that we are as specific as possible about the arguments. So we select the problem direction of each argument. And we select as specific as possible a sub-type of client for each of the arguments. And if we even claim sub-types can't do it now, then we can continue and use pre and post conditions to declare new stronger constraints. In my example here, that's nice simple and as probably able to take that out, except in self-example, increment, procedure to increment the calendar. So, well, the calendar has been implemented so it first has to go in, to modify it, go out again. And we say we want to do it with arbitrary steps. So that's something that the calendar has to go in. And, well, the first thing to do is, well, actually counting, we start from zero, it can't be less. That's natural numbers. And we say we're incrementing. So the step can't be zero or less. So it's a positive number. These are predefined sub-types of integer and data by the way. So now we've put some constraints here, my calendar, and step size. This is something you always need to do in ADEA. Some of the next steps that here, that's a, well, specifically, well, we put in a precondition. Since we've been incrementing, the calendar can't already be the last possible value of our integers. And the first condition, one that will definitely be more than zero. And, but, we can do better than that if we really want to. And so, we can go, let's say we should have steps which will make the calendar go beyond natural marks. The other one is really some set of this one, but that's a math exercise and we're not about to do that today. So that was the first step with our sub-programs looking at the arguments. Next step, that's one of the requirements of our sub-programs which preconditions do we have. Are there any special requirements which should be played before we call a sub-program? A sub-program only be called once in the whole run of the application and it only be called when the application is in specific state. And this is what we can document and put preconditions to a sub-program. Here first, I go back to the test I owe example where writing to a file, we have preconditions, files should be open. But it should also be a file and writing to a certain name that would be an alt file or any file. And another example that here, I imagine I have a variable function telling me about the state of the system and initialize should only be called if the system is non-ish initialized state. When I get to the work of an actual life source example, we'll have something like that to look at because this the part in the API that DJ has provided me with, that's good, I like that. Thanks for working on it. And then the next step back, so looking at life sequences of calls, so we have our types, we have our sub-programs, functions, features. What are the life sequences of calls in these sub-programs? And specifically, will these sequences, as the promises from the first one, does that include the preconditions and the next one being called so on in the chain? So we want to call, initialize blocks, say, shut down. It has a precondition that the system is initialized and initialized doesn't have the post-condition that the system is initialized. We have a problem. So that tells us how we figure out how to add those conditions. We can see that, yes, we have to find the preconditions. Here, we have the precondition initialized. Shut down, post-condition. This is a case which was marked with a lot of black toad, so it tells us that we're not messing with the interstitial state blocks. And shut down, it's not initialized long enough to run initialized again. So we could have things like that shut down. Sorry, I forgot to use two types of lines also. That's a different example. Here we have another called sequence that's open a file, write a file, write in close a file, which makes it easy at the last point to say more than one side. So we say the line has a precondition that requires it to be open. Well, that means that open should have post-conditions that the file is open. And that makes sense. Actually, the way the world works is, well, it might be open, or it might be raising its exception. There's more than any error that we can get out of open, but we didn't have enough lines here. So, it has this, we can call open and then try it, but actually in between we have to be, we have to be prepared and let me end up down in the exception panel and set to do something else about the exceptions. But if the globe goes through, open, then we will know that it is open when we get down here. Everything's fine. But it's, this exercise, it's, in a way, it's relatively trivial, but it's actually making up these sequences of lines, the line-to-sequences of calls. When you have the line-to-sequences of calls, it's where it's trivial. Supposedly trivial. But still, you have to do it. And then, it's time for some source code. I didn't try it myself, so... It's not written quite for this purpose, but rather for static analysis. It's Aero materials. This is a simulator of a sanctified experiment. The drawing signed down from the chart that is falling down and where the slope is too steep, the signs will fall down as they're simply not to one side, always to one side, all in cases. This is just to show the running application. Then the main body of the system. So it starts as solar consummation. Then there's a loop of updating it, adding it right next. Then showing, then getting it to take the radiative plate and then zeroing stuff up at the end. What happens if somehow the rocket gets called to start? What we get, we get an access check, which means that there's a pointer somewhere inside of this library that we're using, which is null and has nothing allocated on it. It is a closer way to start. Another option to be that we actually make sure that we keep track of the state of our simulator like this. Then we'll still get an exception, but it will be caught if I allow the system to be caught. It wouldn't caught when we go out the end of the loop, really, when we try to add a grain that we know that may not initialize. So in source it's a different place. In microseconds of operations on the computer, there's another big difference. Once we get the checking tools in place, when we run the spark verify on it, it will make a difference. Then we'll get a time change. The pre-division term match up. So what I need to do is I just as a demonstration go in to putting some state management like I indicated here in this library. I'll show you what we get now. It's not a minus sign error, unfortunately, but we get a different error in this issue. It's big enough that everybody can read, right? And it's still big enough that everybody can read. Also in the back row. So this is the specification, the external specification of the cellular operator simulator. So the software lattice that we're operating on, it has a kind of, I'm saying, source where we're putting in sand. And some parameters, shading the decisions. That's in part here. And then we have the actual operations. Starting and stopping, adding the grain going to next step in the iteration and showing the right state. But without any pre and post conditions. So what we could do is that we could, we, I would start to say with a finite line describing the state of the automation. And what could it be, be uninitialized? It can be switching. So this is just the type of kinds of states we see here. I've cheated and built inside it and as far as I can see, after we've had started off again, that's why I don't have a separate state. It can be uninitialized before having started again. Then we want to be able to check after back the state. So we just specify a function that returns an alternation state. And now we actually have enough information up here that we can start to add post conditions, first three tomorrow operations. We can see the problem with procedure. So we say, well there's no parameters, so that's not the case. All work in that new general state. So we say we start, or start procedure has a post condition which is that it is initialized. What? State equal to initialize. Yes. Exactly. And somebody remembers. It's uninitialized. And the other one, they don't change anything. So this is what we have of my first state and what are the post conditions. So, going back to... That's because I said what do we do. I'm not doing it right. Because really what we should say is that what do we need? You didn't call all the errors. So if you're just going to add a brain, you can only do that. So we've got the constraint error. We have the condition that we are initializing. State is initializing. And the same is the case for text that shows we've not initialized the test work. So, how complete are we now? State we say that what we do is we say start. And then we say path brain. Then we say next. Then we may say show. And then we may go back here sometimes. And then sometimes we say stop. And pre-conditions here that is initialized. And we can't... the start by extra time to be allocated. And if it tries to do that, we better be initialized. And start it's good to be initialized because otherwise I know there will be a memory. And some of you are wondering why I put in the switching state in between. It's because behind the scenes there's actually a task here. So we have a parallel processing program. So in case some function somewhere might be asking why we are changing the states. We better add the first notes and say which switching state at the moment. Which means that I really have to make the variable where I keep track of the state to properly be atomic. And we could just do that variable in here. Notice this private... the package specification is separated in the public part which is one that the users of the package can see. And the private part which focuses on details about the data modeling. But you can also set variables in the private part instead of only proving that all the way to the implementation. That's the case. 10 minutes left. Actually 5 minutes. If you allow time for questions. We should have these 5 for questions. So when we go to a future... what did we say we said? And then... start. Probably this classical apple of atomic. Then you sex, adding a brain next to a shirt as pre-peditions of the initialized. That's good. And we're putting it in the data frame that we have on the PS. So, staff after we call staff, we are initialized. And after we call staff, we are initialized. So, we have a pre-pedition for this sequence, we have a pre-pedition and it's included in the post-edition of staff at this time. Next, as pre-pedition is not included in the post-edition yet, if we had to control a data flow, it wouldn't be a problem because we know that it doesn't change the state. But we better hear, go in and say, well, actually the post-edition of that, we're still initialized. So, just to make sure that we don't get the problem, what's next? Now, we actually have an option to do something interesting. We can really implement this function here, giving us those main states. So, we have something about making current states. So, now we've set what we do. We have an assertion failure, which basically means that one of our contracts were wrong. And it says, Senator Hussamason, he gets 40. Anybody who kept striking up that they are able to tell us which one that is. So, that a great phase. I'm surprised because you removed the initialization. Yes, but what surprises me is that I had expected the post-edition of staff to be the one that failed. But you never cool-stopped. I removed that call. That's fine. Yes. So, maybe we should go in and... So, we get the line error, yes. So, we go in and activate staff. And now we have something that blocks out. Do we have any... Where did you go? Are there any race conditions in your application again? Yes, sir. Okay, first position. So, now we get an assertion failure, but if there's a mild warning, we should get an assertion failure exiting the information staff. So, now we go in and say, not that we talked about this stage, but we'll actually go in and say... Now it runs. Now, when I ask you to stop by pressing Q, we will enter stop. And stop, well, stop fine, but then since we have not said I'm initialized, then we should get an assertion error. Failed post-edition, line 37. Yes. So, we can see that we can work. We can play around with these post-editions. And we still have a few seconds. I'll go and notice. I'll stop now. Bad style. In Ada, you can declare enumerated types as I did for the automation state. So, a case like this, you really made a state type, which is empty, settled. And then you write out this representation array with the characters also making sure that you set the empty, gives you space, and settles it. Okay, so, that's it. And then there's not so much, but loads of arms, I think, I've set. And you can find the source code examples here, my website there. And then I'll put my slides on my website. All the slides, who? Yeah, so I'll publish mine in a few minutes. How I know how they are when I take the presentation. Any questions? Any which are short enough? I was just wondering about this example with an invariant that guarantees that a point is on a unit dit. I was wondering, where is this check actually enforced and how will that impact performance? Or whether I can even use such a complicated, let's say, invariant in practice? It is forced. Let's see. Subprogram, exits, type conversion. Yeah, it's basically for each time you access the interface, which is anytime you have a... It's either something which could change it. Right. Yeah, type conversion. Type conversion and returning from subprogram. I'll give the result from the program. One that has it as a return value of terms. If it's just an unit, nothing will be done. But yes, it might impact performance. My view is a preferred site and store program which give me a correct result. If I want one that gives me a correct result, I can do it pretty quickly anywhere in the world. I'm sorry, I missed the beginning of your speech. But I'm an expert programmer, so we have... You have stuff like this for a long time. One of the issues in that thing there are things about regularity of calls in evasion of the regulation of a program. Yeah, I... It is resolved. I can't remember the details and I'm not one of the people who have kept it from any of us. Jose, can you remember the details about the standard results issue? No, I'll remember that. I'm pretty sure you have seen something exciting about how to resolve that issue. Yes. But I can't remember the details. Okay, that's true. Yeah. So, I'm sorry, I can't have you with the details there. I wouldn't mind trying to figure it out. I think the problem you mentioned is when you have something like stack full with a precondition, not stack empty. And stack empty with a precondition, not stack full. That's right. And I thought if I remember correctly, accessions are disabled when you are checking another accession. Yes, and limitations differs depending on providers. It arrives when, for example, you say, okay, my result is not the result of the function that is prefixed with an auto. Well, that's what I said. Entity implies not full and full implies not empty. I remember we discussed that during the language. I can assure you that there is nothing like disabling in certain contexts. Now, how will you solve that one? I mentioned this morning that the reference manual is freely available. No, no, no. Also, you have an HTML version of that. And you have another one which is called the annotated reference manual. And in addition to the nomadic text, you have comments that explain the rationale, the decision, and the things that have been discussed when designing the standard. So in a case like that, the best thing is to refer to the annotated reference manual. There is certainly something about that. It doesn't say recursive. I haven't got the annotated installed. I could of course, I explained the network. Well, just annotated in the reference manual. Yeah, but I turned on the network so I wasn't disturbed about presenting. I think we should do that online because we have another presentation coming up now. Let's look it up. And thank you. Thank you. Thank you. Thank you.
 So I'll put on this as a tutorial.  We'll start out tomorrow as a common presentation.  And I have an example.  I did it.  It was going to give me an example.  So I didn't make up an example.  I healed the task, but I didn't have to work on two wheels.  But I'm going to talk about how to use.  I think you should use the aspects of implementation programming  in the media stuff.  So just so I sort of know, how many of you have not programmed  in it at all?  OK.  That's good to know.  If you happen to hear either some peers talk this morning  or the previous one, OK, so how do you think what you said about it?  I don't.  Me, I'm independent and sometimes I'm not really doing software development stuff,  but also interesting thing like inspecting mobile platforms  and starting up with new games, starting finance.  And well, since we have all heard about that much about data before,  I'll just say some of the reasons why we should be using data.  I need to design on this data of seeing programming as a human security  about reliability and about maintenance.  Contracts in data that mostly are reliability and maintenance  as the contract is form of documentation,  which has added benefit of actually being checked by the client  the entire time or other time, so it's really reliability and way.  That's a very short story about ADEN.  Then I have a presentation of ADEN in a simple slide,  which is not enough to learn about ADEN,  but you can get an idea about it.  Is procedural programming language  is a form of public-dialogical programming?  You're not forced to use public-dialogical programming, but you can do it.  There's what you call multiple programming.  You can separate your project packages, file packages.  You have individual standards on some programs.  There's generics, which is an alternative to public-dialogical programming  that's what generalizes your solutions.  One thing that I like very much,  and it's also very relevant about time management,  is the separation of declarations of top programs and packages  and the actual implementation of them.  First, you specify the interface,  then separate from that, we write back the documentation  just to make sure you're doing the right thing.  We have to repeat the basics of the specification.  Then, as the current speaker,  we will have programming facilities to go into the language,  not just the hospital, not just ad-on languages,  but actually as a part of the language specification.  Then, in 1997,  I have something to think of as a name,  rather than just by what value status  the hospital's running for.  It comes at a time like 40 classes in our technical program,  and for simple times,  like various people do at home,  on other times.  The most recent standard was published,  more or less, and they did not publish in 1990.  What is it?  In 1990, first grade,  50% of 2012,  the initial course in the human history.  But then,  the regulations are on the 12 standard,  only one in the series.  Some of this, which is new,  exactly about the basic programming,  that's the ability to prepare  pre and first conditions for sub-programs,  which is, as a minimum,  the long-term runtime checks  and the state of parameters for sub-programs  before and after a phone.  Then there's time variance  and sub-time predicates,  which are the kinds of constraints  which should be consistent for all updates  and there's time, time at all times.  The differences between these three  is the time variance, like checks and private types,  where you have  in-vay implementation details,  exactly which components exist at this time,  where predicates that for  technically for sub-types,  but for types where you have visibility  in the terminals,  and they act more as constraints  and different dynamic constraints,  that is related to how easy it is  basically to do a compile time analysis.  I have an example later on where you'll see  that with compiler,  actually already with an app,  TPO 2013 edition,  and a patch,  is that compile time programming error,  in a case where it's done in some time predicates.  Hopefully in the future we'll have  more of the smart tool facilities  migrating into the compiler  so we'll have messages when you compile.  Well, your program's available in the country running,  but this line, the policy,  you're not fulfilling some condition.  But we're not quite there yet.  So you'll go back to Paris to work on it soon.  If you do not the thing that people will say,  oh, the compiler is just a wall now.  Well, yes, I have...  So now you still have to run various tools,  besides the client,  yes, in time time.  But besides all this new and fancy stuff,  you have the data programmers,  makers, and the input tool.  But also, we have the name,  primitive types.  If you have specific type,  even if you have another type  with exactly the same values,  you can't just copy  between objects at the same time.  You have to make explicit conversions.  You have currently the passing directions  on your subprogram.  So you have to tell explicitly  if an argument for a subprogram  is apparently going in,  apparently they're going out.  Like, one that's going both ways,  and then out after some time in the page.  And then we have the rate checks on the rates.  So you don't accidentally call  on the vercos in address, outside, and array.  And then we have sub-times,  which is basically having an existing type  and then make a subset of it for the ranges.  And then there's some cases where  you have static checks,  like that a case statement  covers all the possible values of document  for case statements.  You get a complaint and an email error  because of how many of these are all the possible values.  Some of this is higher time checks.  Some of this is one-time checks.  But it all helps.  Catching errors earlier and later.  And there is the better.  I've used contracts on a  medium-sized product,  but it's the last year and a half.  And I must admit that even though we're using them,  I'm not sure we've actually called any errors  directly by the pilot saying he did something wrong.  Must admit that.  But it could be because we have good programmers.  It could also be because they're not assigning  the final contracts that much against us.  So now I'll start going through  each kind of contract elements.  We have in data 2012  come up with some comments and a small example.  We'll start with a pre-condition  and from the rationale for the data result  it's an application under form.  All of us ensure that something is in order  before you form the sub-program.  And it's a guarantee that if you're going to  implement the sub-program like this,  this is true once you're formed.  And I just came up with an example.  Eating data from the pilot,  but haven't actually put any of these contract aspects  much of the standard libraries.  So I decided to just take some examples  from the take my own API data.  So we say we want to put a spring to a context file.  Well, we better make sure the file is open first.  So this is one example you can put in on a pre-condition.  Still, in this case, we could of course  have a race condition that, well,  once we call it, it's okay,  but there always is marked file system  or makes some strange things.  Meanwhile, so the abrasion can still fail in these cases.  But it's a nice minimal requirement in the case.  Similarly, in your first conditions,  you're staying half done, talking to us  when you're calling a sub-program.  That's an obligation and the incumbent  of the sub-program to make sure that this is true  once the sub-program returns.  And it's a promise, a lot of hands to the call,  and that this is how the world will be afterwards.  And I decided then, okay, let's take the line  and we can take the IO API.  And data has, depending on your view,  an eyes or an eye, an eye,  and a house of feature,  a keeping track of line numbers  and the file when you're writing through it,  a reading from it.  So actually, we can say that after you've done the line,  the line number has been implemented by one.  So that's an example of a post-condition.  Here, I reference the value of the line number  before calling through this item node.  Yeah, I'm not going to teach you the details  of the syntax of data in this talk.  That would take more than an hour.  So there are lots of good references for that.  That was three post-conditions then.  Time in arrays.  This is an example I've adapted from the 2012 rationale.  Imagine you want to have,  we've got 12 reactions.  We want to have the time in,  the time in through a percentage function of the unit.  That was the mathematician one.  The function is earlier.  We can start by just saying,  well, we do it in random vector,  and we'll have four names.  Yeah.  But then,  flow then, you can see anywhere,  then with the limit times minus one to one,  and we get it into this box here.  But we don't want it turned off here.  We can do that with time in arrays  that the distance from the cargo shouldn't go beyond one.  So now we have the type here  for managing the response of the unit base.  Of course, there could be  any type of conditions here.  But the point is that this is something that  the compiler now is obliged to do  to objects of type this point.  But it always has to be true.  Yeah.  You go back here.  That's good.  Very good.  A good point derived from one that was just  an arbitrary point where you'd say,  okay, it can be anywhere as far as  building point type for the sense.  And then we use this as a subtype,  the subtype constraint.  Then the kind of variance  that's dynamic in subtype predicates.  That's kind of constraints  in sub-setting subtypes.  If you look at an example here, a prime,  it's an integer.  It can't be less than two.  And you can't have any factors  to the number which are different from  one and the number itself.  Which if we look at the here, we're saying  that prime line was n to zero.  That happens for some n from two  up to prime minus one.  Then it's not the R dynamic predicate.  It's not the truth.  So now we have a subtype of integers  which is only the prime.  Unfortunately, you can't do fancy stuff  by looping over a subtype of the dynamic predicate.  You can do that with the standard predicate.  But you can have these made.  Now you can just, the lazy test now  for which integers are prime  is to just loop over all the integers  and see if you can, it's in the subtype prime.  Because it's not necessarily  computationally efficient, but that's a different matter.  This is an example of an actual project  where there was a decision somewhere  that this organization Ui could not be  longer than 256 characters.  And to avoid that we accidentally  in our program tried to put a larger string,  longer strings into our database,  we made this subtype where we put in  a dynamic predicate and the length of these strings.  In older versions of A8, you could do something similar  by creating a bounded string  which would have length of 256 characters.  But all the work during that, this is much easier.  And then, I said before it was dynamic,  subtype predicate.  Subtype predicate, they are more limited in what,  basically it's the same, but it's more limited  with expressions you're allowed to use.  You can do anything where your subtype  is in a statically defined sense  or part of an otherwise static expression.  There's some operations you can do at least.  It's not all.  But this is one of the cases, look it up  in the reference manual when you get to it.  And I was in Mauritius recently working  for a small data company there.  So I decided, well, we'll make a nice example  of the summer burn from November to April.  How was the end of the week?  That's a different story.  So now we have a type of month,  just made a short business,  an example of an operation time to data.  And then I make a subtype where I say,  okay, the summer month, that's in November to December  and then from January to April.  And then I declare an update.  And then I accidentally switch back to  northern chemistry mode and say,  well, July is the summer month,  but trying that with a compiler,  you get the warning group that doesn't work.  You get a failure because July is not  the summer subtype.  There's a similar example in the  government program, no,  but it's by grid fire and Englishman  that is clearly not used to the concept  that the summer could go from November to April.  So it does, with a window from December  to January, the very exact effect is the same.  And then I talk about coverage change.  Here I have a, well, not very nice example  of a case statement.  Level is, if there's the level of  some of the logic messages, which is the  very true level, and then we say  the different operations which we're  to send the messages depending on the level.  It's split out to the case-thens statement,  but what would happen if I accidentally  forgot to put in the alert level?  What would happen would be that the  island would say that I'm not telling  all the possible values of the  tidal level and it would stop  from crying in my program.  I'd have to go P.A. and do something.  It's not directly contract, but it's a  very useful static implementation check.  And it relates to the subtype of this  value you put in.  So that was the quicker overview of  contracts in April 2012.  Now, say I look like this senior,  I've got everything included.  Yeah.  Okay.  I've got my best to put some guidelines  together to get a consistent use of  contract-based programming in AIDA.  When I started, I just put things in  and write them on a sort of .NET file.  We can put something in here.  It's better if you do it consistently  across the application or your library.  And the place I like to start when I'm  programming, that's with the types.  So, make sure that you make good detailed  declaration of the type and its constraints.  You declare type or subtype depending on  the requirements of compatibility with  other types.  You want to be fast-directed or if it  should be really unique type that you  should expect to be back and forth.  You can put appropriate constraints in  your values.  I had the example where the point  squared was the constraint that the  30-point coordinate shouldn't be less  than minus 1 at the end point as an  example.  And then you can add extra examples,  extra constraints, any displeasure as  predicates or varies in the type.  But I think you'll see that in many  cases you don't really need that.  This is enough in the kind of other  contracts for a time.  So, I go back to my introduced in my  primary example.  We start off with this, crime-plated  introduced.  And I decided here that, well, it's  really an integer.  It's not that special.  So it's just a subtype of integer.  If I thought it was really something  special, I would say crime type crime  is new integer and it would be a new  type just having to be derived from  integer time.  And then there's this about crime  is being largely done one after the  range constraint done.  And crime is a nice approach.  That's not enough.  We also need to keep track of the  only factors that's one of the  crimes itself.  So, an example, Native Country,  these items, I have to say so, I  have used it in real-time.  I did use Spark once to validate  applications of my crimes.  And it found an error.  I hadn't found it by testing.  I was impatient.  If I had to let it try to run to the  end, it would have faded around  there because there was some  mismatch running over the edge of  the number of that integer in  the process.  It took some time to figure out that  it was that that Spark was telling  you it was wrong.  It's definitely useful and it's useful  in cases where you have the patients  to find it by testing.  I know also that the Spark people  are being involved in testing a  cryptographic hash function where  there's a Spark in the reference  implementation.  If you give it 2 to the 64, 5 long  data sets to hash, it gets the wrong  value.  And nobody apparently have tested  that.  So the bug is still there, though it  has been reported.  But then, back to the main story,  now we have declared our times.  The next step, that's the sub-programs  which are going to operate in these  times.  And not going to inter-detail on the  sub-programs themselves.  But when we have no which one we  need, make sure that we are as  specific as possible about the  arguments.  So we select the problem direction  of each argument.  And we select as specific as  possible a sub-type of client  for each of the arguments.  And if we even claim sub-types  can't do it now, then we can  continue and use pre and post  conditions to declare new  stronger constraints.  In my example here, that's nice  simple and as probably able to  take that out, except in  self-example, increment, procedure  to increment the calendar.  So, well, the calendar has been  implemented so it first has to go  in, to modify it, go out again.  And we say we want to do it with  arbitrary steps.  So that's something that  the calendar has to go in.  And, well, the first thing to do  is, well, actually counting, we  start from zero, it can't be less.  That's natural numbers.  And we say we're incrementing.  So the step can't be zero or less.  So it's a positive number.  These are predefined sub-types  of integer and data by the way.  So now we've put some constraints  here, my calendar, and step size.  This is something you always  need to do in ADEA.  Some of the next steps that  here, that's a, well, specifically,  well, we put in a precondition.  Since we've been incrementing,  the calendar can't already be  the last possible value of our  integers.  And the first condition, one  that will definitely be more than  zero.  And, but, we can do better than  that if we really want to.  And so, we can go, let's say  we should have steps which will  make the calendar go beyond natural  marks.  The other one is really some  set of this one, but that's  a math exercise and we're not  about to do that today.  So that was the first step  with our sub-programs  looking at the arguments.  Next step, that's one of the  requirements of our sub-programs  which preconditions do we have.  Are there any special requirements  which should be played before  we call a sub-program?  A sub-program only be called once  in the whole run of the application  and it only be called when the  application is in specific state.  And this is what we can document  and put preconditions to a sub-program.  Here first, I go back to the  test I owe example where  writing to a file, we have  preconditions, files should be open.  But it should also be a file  and writing to a certain  name that would be an  alt file or any file.  And another example that here,  I imagine I have a variable  function telling me about the  state of the system and initialize  should only be called if the  system is non-ish initialized state.  When I get to the work of an  actual life source example,  we'll have something like that  to look at because this  the part in the API that  DJ has provided me with,  that's good, I like that.  Thanks for working on it.  And then the next step back,  so looking at life sequences of  calls, so we have our  types, we have our sub-programs,  functions, features.  What are the life sequences  of calls in these sub-programs?  And specifically, will these  sequences, as the promises from  the first one, does that  include the preconditions and  the next one being called  so on in the chain?  So we want to call,  initialize  blocks, say, shut down.  It has a precondition that the system is initialized  and initialized doesn't have the  post-condition that the system is initialized.  We have a problem.  So that tells us how we figure out  how to add those conditions.  We can see that, yes,  we have to find the preconditions.  Here,  we have the precondition initialized.  Shut down,  post-condition.  This is a case which was marked with  a lot of black toad,  so it tells us that we're not messing  with the interstitial state blocks.  And shut down,  it's not initialized long enough  to run initialized again.  So we could have things like that  shut down.  Sorry, I forgot to use  two types of lines also.  That's a different example.  Here we have another called  sequence that's open a file,  write a file,  write in close a file,  which makes it easy at the last point  to say more than one side.  So we say the line has a precondition  that requires it to be open.  Well, that means that open  should have post-conditions that  the file is open.  And that makes sense.  Actually, the way the world works is,  well, it might be open,  or it might be raising its exception.  There's more than any error that  we can get out of open,  but we didn't have enough lines here.  So, it has this, we can call  open and then try it,  but actually in between we have to be,  we have to be prepared  and let me end up down in the exception  panel and set to do something else  about the exceptions.  But if the globe goes through,  open,  then we will know that it is open  when we get down here.  Everything's fine.  But it's, this exercise,  it's, in a way, it's relatively trivial,  but it's actually making up  these sequences of lines,  the line-to-sequences of calls.  When you have the line-to-sequences of calls,  it's where it's trivial.  Supposedly trivial.  But still, you have to do it.  And then, it's time for some source code.  I didn't try it myself, so...  It's not written  quite for this purpose,  but rather for static analysis.  It's Aero materials.  This is a simulator of a sanctified experiment.  The drawing signed down from the chart that is falling down and where the slope is too steep,  the signs will fall down as they're simply not to one side, always to one side, all in cases.  This is just to show the running application.  Then the main body of the system.  So it starts as solar consummation.  Then there's a loop of updating it, adding it right next.  Then showing, then getting it to take the radiative plate and then zeroing stuff up at the end.  What happens if somehow the rocket gets called to start?  What we get, we get an access check, which means that there's a pointer somewhere inside of this library that we're using,  which is null and has nothing allocated on it.  It is a closer way to start.  Another option to be that we actually make sure that we keep track of the state of our simulator like this.  Then we'll still get an exception, but it will be caught if I allow the system to be caught.  It wouldn't caught when we go out the end of the loop, really, when we try to add a grain that we know that may not initialize.  So in source it's a different place.  In microseconds of operations on the computer, there's another big difference.  Once we get the checking tools in place, when we run the spark verify on it, it will make a difference.  Then we'll get a time change.  The pre-division term match up.  So what I need to do is I just as a demonstration go in to putting some state management like I indicated here in this library.  I'll show you what we get now. It's not a minus sign error, unfortunately, but we get a different error in this issue.  It's big enough that everybody can read, right?  And it's still big enough that everybody can read.  Also in the back row.  So this is the specification, the external specification of the cellular operator simulator.  So the software lattice that we're operating on, it has a kind of, I'm saying, source where we're putting in sand.  And some parameters, shading the decisions.  That's in part here.  And then we have the actual operations.  Starting and stopping, adding the grain going to next step in the iteration and showing the right state.  But without any pre and post conditions.  So what we could do is that we could, we, I would start to say with a finite line describing the state of the automation.  And what could it be, be uninitialized?  It can be switching.  So this is just the type of kinds of states we see here.  I've cheated and built inside it and as far as I can see, after we've had started off again, that's why I don't have a separate state.  It can be uninitialized before having started again.  Then we want to be able to check after back the state.  So we just specify a function that returns an alternation state.  And now we actually have enough information up here that we can start to add post conditions, first three tomorrow operations.  We can see the problem with procedure.  So we say, well there's no parameters, so that's not the case.  All work in that new general state.  So we say we start, or start procedure has a post condition which is that it is initialized.  What?  State equal to initialize.  Yes.  Exactly.  And somebody remembers.  It's uninitialized.  And the other one, they don't change anything.  So this is what we have of my first state and what are the post conditions.  So, going back to...  That's because I said what do we do. I'm not doing it right.  Because really what we should say is that what do we need?  You didn't call all the errors.  So if you're just going to add a brain, you can only do that.  So we've got the constraint error.  We have the condition that we are initializing.  State is initializing.  And the same is the case for text that shows we've not initialized the test work.  So, how complete are we now?  State we say that what we do is we say start.  And then we say path brain. Then we say next.  Then we may say show.  And then we may go back here sometimes.  And then sometimes we say stop.  And pre-conditions here that is initialized.  And we can't... the start by extra time to be allocated.  And if it tries to do that, we better be initialized.  And start it's good to be initialized because otherwise I know there will be a memory.  And some of you are wondering why I put in the switching state in between.  It's because behind the scenes there's actually a task here.  So we have a parallel processing program.  So in case some function somewhere might be asking why we are changing the states.  We better add the first notes and say which switching state at the moment.  Which means that I really have to make the variable where I keep track of the state to properly be atomic.  And we could just do that variable in here.  Notice this private... the package specification is separated in the public part which is one that the users of the package can see.  And the private part which focuses on details about the data modeling.  But you can also set variables in the private part instead of only proving that all the way to the implementation.  That's the case.  10 minutes left. Actually 5 minutes.  If you allow time for questions.  We should have these 5 for questions.  So when we go to a future... what did we say we said?  And then... start. Probably this classical apple of atomic.  Then you sex, adding a brain next to a shirt as pre-peditions of the initialized.  That's good. And we're putting it in the data frame that we have on the PS.  So, staff after we call staff, we are initialized.  And after we call staff, we are initialized.  So, we have a pre-pedition for this sequence, we have a pre-pedition and it's included in the post-edition of staff at this time.  Next, as pre-pedition is not included in the post-edition yet, if we had to control a data flow, it wouldn't be a problem because we know that it doesn't change the state.  But we better hear, go in and say, well, actually the post-edition of that, we're still initialized.  So, just to make sure that we don't get the problem, what's next?  Now, we actually have an option to do something interesting.  We can really implement this function here, giving us those main states.  So, we have something about making current states.  So, now we've set what we do.  We have an assertion failure, which basically means that one of our contracts were wrong. And it says, Senator Hussamason, he gets 40.  Anybody who kept striking up that they are able to tell us which one that is.  So, that a great phase.  I'm surprised because you removed the initialization.  Yes, but what surprises me is that I had expected the post-edition of staff to be the one that failed.  But you never cool-stopped.  I removed that call.  That's fine. Yes.  So, maybe we should go in and...  So, we get the line error, yes.  So, we go in and activate staff.  And now we have something that blocks out.  Do we have any...  Where did you go?  Are there any race conditions in your application again?  Yes, sir.  Okay, first position.  So, now we get an assertion failure, but if there's a mild warning, we should get an assertion failure exiting the information staff.  So, now we go in and say, not that we talked about this stage, but we'll actually go in and say...  Now it runs.  Now, when I ask you to stop by pressing Q, we will enter stop.  And stop, well, stop fine, but then since we have not said I'm initialized, then we should get an assertion error.  Failed post-edition, line 37.  Yes.  So, we can see that we can work.  We can play around with these post-editions.  And we still have a few seconds.  I'll go and notice.  I'll stop now.  Bad style.  In Ada, you can declare enumerated types as I did for the automation state.  So, a case like this, you really made a state type, which is empty, settled.  And then you write out this representation array with the characters also making sure that you set the empty, gives you space, and settles it.  Okay, so, that's it.  And then there's not so much, but loads of arms, I think, I've set.  And you can find the source code examples here, my website there.  And then I'll put my slides on my website.  All the slides, who?  Yeah, so I'll publish mine in a few minutes.  How I know how they are when I take the presentation.  Any questions?  Any which are short enough?  I was just wondering about this example with an invariant that guarantees that a point is on a unit dit.  I was wondering, where is this check actually enforced and how will that impact performance?  Or whether I can even use such a complicated, let's say, invariant in practice?  It is forced.  Let's see.  Subprogram, exits, type conversion.  Yeah, it's basically for each time you access the interface, which is anytime you have a...  It's either something which could change it.  Right.  Yeah, type conversion.  Type conversion and returning from subprogram.  I'll give the result from the program.  One that has it as a return value of terms.  If it's just an unit, nothing will be done.  But yes, it might impact performance.  My view is a preferred site and store program which give me a correct result.  If I want one that gives me a correct result, I can do it pretty quickly anywhere in the world.  I'm sorry, I missed the beginning of your speech.  But I'm an expert programmer, so we have...  You have stuff like this for a long time.  One of the issues in that thing there are things about regularity of calls in evasion of the regulation of a program.  Yeah, I...  It is resolved.  I can't remember the details and I'm not one of the people who have kept it from any of us.  Jose, can you remember the details about the standard results issue?  No, I'll remember that.  I'm pretty sure you have seen something exciting about how to resolve that issue.  Yes.  But I can't remember the details.  Okay, that's true.  Yeah.  So, I'm sorry, I can't have you with the details there.  I wouldn't mind trying to figure it out.  I think the problem you mentioned is when you have something like stack full with a precondition, not stack empty.  And stack empty with a precondition, not stack full.  That's right.  And I thought if I remember correctly, accessions are disabled when you are checking another accession.  Yes, and limitations differs depending on providers.  It arrives when, for example, you say, okay, my result is not the result of the function that is prefixed with an auto.  Well, that's what I said.  Entity implies not full and full implies not empty.  I remember we discussed that during the language.  I can assure you that there is nothing like disabling in certain contexts.  Now, how will you solve that one?  I mentioned this morning that the reference manual is freely available.  No, no, no.  Also, you have an HTML version of that.  And you have another one which is called the annotated reference manual.  And in addition to the nomadic text, you have comments that explain the rationale, the decision, and the things that have been discussed when designing the standard.  So in a case like that, the best thing is to refer to the annotated reference manual.  There is certainly something about that.  It doesn't say recursive.  I haven't got the annotated installed.  I could of course, I explained the network.  Well, just annotated in the reference manual.  Yeah, but I turned on the network so I wasn't disturbed about presenting.  I think we should do that online because we have another presentation coming up now.  Let's look it up.  And thank you.  Thank you.  Thank you.  Thank you.
_FOSDEM_2014__Contract_Based_Programming_in_Ada_2012_EjC3QjHuAFY_0_2291.png _FOSDEM_2014__Contract_Based_Programming_in_Ada_2012_EjC3QjHuAFY_2292_2855.png _FOSDEM_2014__Contract_Based_Programming_in_Ada_2012_EjC3QjHuAFY_2856_21743.png _FOSDEM_2014__Contract_Based_Programming_in_Ada_2012_EjC3QjHuAFY_21744_21803.png _FOSDEM_2014__Contract_Based_Programming_in_Ada_2012_EjC3QjHuAFY_21804_21899.png _FOSDEM_2014__Contract_Based_Programming_in_Ada_2012_EjC3QjHuAFY_21900_21983.png _FOSDEM_2014__Contract_Based_Programming_in_Ada_2012_EjC3QjHuAFY_21984_22355.png _FOSDEM_2014__Contract_Based_Programming_in_Ada_2012_EjC3QjHuAFY_22356_30695.png _FOSDEM_2014__Contract_Based_Programming_in_Ada_2012_EjC3QjHuAFY_30696_31487.png _FOSDEM_2014__Contract_Based_Programming_in_Ada_2012_EjC3QjHuAFY_31488_50615.png _FOSDEM_2014__Contract_Based_Programming_in_Ada_2012_EjC3QjHuAFY_50616_51791.png _FOSDEM_2014__Contract_Based_Programming_in_Ada_2012_EjC3QjHuAFY_51792_52223.png _FOSDEM_2014__Contract_Based_Programming_in_Ada_2012_EjC3QjHuAFY_52224_52391.png _FOSDEM_2014__Contract_Based_Programming_in_Ada_2012_EjC3QjHuAFY_52392_52607.png _FOSDEM_2014__Contract_Based_Programming_in_Ada_2012_EjC3QjHuAFY_52608_53303.png _FOSDEM_2014__Contract_Based_Programming_in_Ada_2012_EjC3QjHuAFY_53304_53723.png _FOSDEM_2014__Contract_Based_Programming_in_Ada_2012_EjC3QjHuAFY_53724_53867.png _FOSDEM_2014__Contract_Based_Programming_in_Ada_2012_EjC3QjHuAFY_53868_54191.png _FOSDEM_2014__Contract_Based_Programming_in_Ada_2012_EjC3QjHuAFY_54192_54395.png _FOSDEM_2014__Contract_Based_Programming_in_Ada_2012_EjC3QjHuAFY_54396_54515.png _FOSDEM_2014__Contract_Based_Programming_in_Ada_2012_EjC3QjHuAFY_54516_54575.png _FOSDEM_2014__Contract_Based_Programming_in_Ada_2012_EjC3QjHuAFY_54576_54635.png _FOSDEM_2014__Contract_Based_Programming_in_Ada_2012_EjC3QjHuAFY_54636_54695.png _FOSDEM_2014__Contract_Based_Programming_in_Ada_2012_EjC3QjHuAFY_54696_54887.png _FOSDEM_2014__Contract_Based_Programming_in_Ada_2012_EjC3QjHuAFY_54888_55007.png _FOSDEM_2014__Contract_Based_Programming_in_Ada_2012_EjC3QjHuAFY_55008_55079.png _FOSDEM_2014__Contract_Based_Programming_in_Ada_2012_EjC3QjHuAFY_55080_55187.png _FOSDEM_2014__Contract_Based_Programming_in_Ada_2012_EjC3QjHuAFY_55188_55415.png _FOSDEM_2014__Contract_Based_Programming_in_Ada_2012_EjC3QjHuAFY_55416_55919.png _FOSDEM_2014__Contract_Based_Programming_in_Ada_2012_EjC3QjHuAFY_55920_57107.png _FOSDEM_2014__Contract_Based_Programming_in_Ada_2012_EjC3QjHuAFY_57108_57155.png _FOSDEM_2014__Contract_Based_Programming_in_Ada_2012_EjC3QjHuAFY_57156_57803.png _FOSDEM_2014__Contract_Based_Programming_in_Ada_2012_EjC3QjHuAFY_57804_58451.png _FOSDEM_2014__Contract_Based_Programming_in_Ada_2012_EjC3QjHuAFY_58452_59975.png _FOSDEM_2014__Contract_Based_Programming_in_Ada_2012_EjC3QjHuAFY_59976_60503.png _FOSDEM_2014__Contract_Based_Programming_in_Ada_2012_EjC3QjHuAFY_60504_61595.png _FOSDEM_2014__Contract_Based_Programming_in_Ada_2012_EjC3QjHuAFY_61596_65963.png _FOSDEM_2014__Contract_Based_Programming_in_Ada_2012_EjC3QjHuAFY_65964_66095.png _FOSDEM_2014__Contract_Based_Programming_in_Ada_2012_EjC3QjHuAFY_66096_66143.png _FOSDEM_2014__Contract_Based_Programming_in_Ada_2012_EjC3QjHuAFY_66144_74831.png _FOSDEM_2014__Contract_Based_Programming_in_Ada_2012_EjC3QjHuAFY_74832_75839.png _FOSDEM_2014__Contract_Based_Programming_in_Ada_2012_EjC3QjHuAFY_75840_76259.png _FOSDEM_2014__Contract_Based_Programming_in_Ada_2012_EjC3QjHuAFY_76260_76475.png _FOSDEM_2014__Contract_Based_Programming_in_Ada_2012_EjC3QjHuAFY_76476_76571.png _FOSDEM_2014__Contract_Based_Programming_in_Ada_2012_EjC3QjHuAFY_76572_76679.png _FOSDEM_2014__Contract_Based_Programming_in_Ada_2012_EjC3QjHuAFY_76680_77183.png _FOSDEM_2014__Contract_Based_Programming_in_Ada_2012_EjC3QjHuAFY_77184_77243.png _FOSDEM_2014__Contract_Based_Programming_in_Ada_2012_EjC3QjHuAFY_77244_77831.png _FOSDEM_2014__Contract_Based_Programming_in_Ada_2012_EjC3QjHuAFY_77832_77975.png _FOSDEM_2014__Contract_Based_Programming_in_Ada_2012_EjC3QjHuAFY_77976_78023.png _FOSDEM_2014__Contract_Based_Programming_in_Ada_2012_EjC3QjHuAFY_78024_78599.png _FOSDEM_2014__Contract_Based_Programming_in_Ada_2012_EjC3QjHuAFY_78600_79739.png _FOSDEM_2014__Contract_Based_Programming_in_Ada_2012_EjC3QjHuAFY_79740_79955.png _FOSDEM_2014__Contract_Based_Programming_in_Ada_2012_EjC3QjHuAFY_79956_80663.png _FOSDEM_2014__Contract_Based_Programming_in_Ada_2012_EjC3QjHuAFY_80664_81623.png _FOSDEM_2014__Contract_Based_Programming_in_Ada_2012_EjC3QjHuAFY_81624_81911.png _FOSDEM_2014__Contract_Based_Programming_in_Ada_2012_EjC3QjHuAFY_81912_81971.png _FOSDEM_2014__Contract_Based_Programming_in_Ada_2012_EjC3QjHuAFY_81972_82043.png _FOSDEM_2014__Contract_Based_Programming_in_Ada_2012_EjC3QjHuAFY_82044_82163.png _FOSDEM_2014__Contract_Based_Programming_in_Ada_2012_EjC3QjHuAFY_82164_83327.png _FOSDEM_2014__Contract_Based_Programming_in_Ada_2012_EjC3QjHuAFY_83328_84395.png _FOSDEM_2014__Contract_Based_Programming_in_Ada_2012_EjC3QjHuAFY_84396_91319.png _FOSDEM_2014__Contract_Based_Programming_in_Ada_2012_EjC3QjHuAFY_91320_91415.png _FOSDEM_2014__Contract_Based_Programming_in_Ada_2012_EjC3QjHuAFY_91416_91511.png _FOSDEM_2014__Contract_Based_Programming_in_Ada_2012_EjC3QjHuAFY_91512_91571.png _FOSDEM_2014__Contract_Based_Programming_in_Ada_2012_EjC3QjHuAFY_91572_91643.png _FOSDEM_2014__Contract_Based_Programming_in_Ada_2012_EjC3QjHuAFY_91644_91691.png _FOSDEM_2014__Contract_Based_Programming_in_Ada_2012_EjC3QjHuAFY_91692_91739.png _FOSDEM_2014__Contract_Based_Programming_in_Ada_2012_EjC3QjHuAFY_91740_91799.png _FOSDEM_2014__Contract_Based_Programming_in_Ada_2012_EjC3QjHuAFY_91800_91859.png _FOSDEM_2014__Contract_Based_Programming_in_Ada_2012_EjC3QjHuAFY_91860_91907.png _FOSDEM_2014__Contract_Based_Programming_in_Ada_2012_EjC3QjHuAFY_91908_92961.png