Contract Based Programming in Ada 2012
This is a modal window.
The media could not be loaded, either because the server or network failed or because the format is not supported.
Formal Metadata
| Title |
| |
| Title of Series | ||
| Number of Parts | 199 | |
| Author | ||
| License | 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. | |
| Identifiers | 10.5446/32503 (DOI) | |
| Publisher | ||
| Release Date | ||
| Language |
Content Metadata
| Subject Area | ||
| Genre | ||
| Abstract |
|
FOSDEM 2014109 / 199
2
3
10
11
12
13
14
17
18
19
23
24
25
27
29
45
46
47
48
49
50
51
52
55
56
57
58
65
67
68
70
72
74
75
76
77
78
79
81
82
84
86
87
89
90
93
94
100
101
102
103
104
106
107
109
110
111
112
113
114
115
119
122
123
124
126
127
128
129
137
139
141
143
145
147
150
154
155
158
161
163
164
165
166
168
171
174
175
176
179
182
183
185
188
190
191
192
194
195
196
00:00
IterationLine (geometry)Computer programmingLibrary (computing)Multiplication signVarianceRight angleProbability theoryState of matterMereologyGravitationWordDifferent (Kate Ryan album)Machine codeProgramming languageInvariant (mathematics)Information technology consultingObject-oriented programmingImplementationStandard deviationPredicate (grammar)Modulare ProgrammierungRun time (program lifecycle phase)Presentation of a groupSlide ruleProjective planeParameter (computer programming)Constraint (mathematics)Form (programming)NumberBitCASE <Informatik>Design by contractQuicksortEntire functionPrimitive (album)Declarative programmingCloud computingSoftware maintenanceSoftware developerFluid staticsFlow separationComputer programProcedural programmingConnectivity (graph theory)Message passingNeuroinformatikComputer fileExterior algebraLecture/Conference
08:26
Line (geometry)Parameter (computer programming)Computer programCondition numberMultiplication signPredicate (grammar)Data conversionTrailPoint (geometry)Element (mathematics)IntegerCompilerOrder (biology)Functional programmingConstraint (mathematics)Range (statistics)CASE <Informatik>MiniDiscError messageSubsetBuildingDivisorProjective planeSystem callNumberRatsche <Physik>Array data structureOperator (mathematics)Variable (mathematics)Context awarenessExecution unitComputer fileDataflowBit rateZeitinvariantes SystemStatement (computer science)CuboidDerivation (linguistics)DistanceFile systemObject-oriented programmingDesign by contractLibrary (computing)RankingPrime idealDirection (geometry)Vector spaceString (computer science)AngleInvariant (mathematics)Dynamical systemAreaEndliche ModelltheorieMachine codeDifferent (Kate Ryan album)Group actionMereologyTheoryLocal ringUniverse (mathematics)Water vaporQuicksortVarianceRoutingRight angleMathematical analysisVideo gameMatching (graph theory)XMLUML
16:52
IntegerMultiplication signTable (information)Right angleMereologyPoint (geometry)VideoconferencingGoodness of fitLine (geometry)VarianceState of matterOperator (mathematics)Constraint (mathematics)Computer programmingDecision theoryProjective planeSelf-organizationResultantFamilyFraction (mathematics)Power (physics)View (database)Arithmetic progressionLibrary (computing)WordSampling (statistics)Shape (magazine)WhiteboardPlanningINTEGRALLevel (video gaming)Asynchronous Transfer ModeInvariant (mathematics)SummierbarkeitCartesian coordinate systemFinite differenceWindowCASE <Informatik>Prime idealExpressionSound effectStatement (computer science)Predicate (grammar)Design by contractProgrammschleifeLengthQuicksortObject-oriented programmingBit rateMessage passingComputer fileString (computer science)Beta functionSoftware testingInclusion mapRevision controlSimilarity (geometry)ConsistencyFluid staticsImplementationError messageDatabaseDynamical systemDivisorDeclarative programmingDegree (graph theory)TrailLecture/Conference
25:18
CASE <Informatik>System programmingState of matterDirection (geometry)Web pageMathematicsPreconditionerSubsetPower (physics)SequenceMereologyProcess (computing)Multiplication signSinc functionComputer fileFunctional programmingParameter (computer programming)Natural numberProcedural programmingIntegerCondition number1 (number)ImplementationNumberSoftware bugConstraint (mathematics)Symbol tableSign (mathematics)Source codeSoftware testingCryptographyCartesian coordinate systemHash functionAlgorithmSystem callBuildingWordQuicksortLevel (video gaming)Line (geometry)Social classRight angleProof theoryComputer programmingMassArithmetic meanGreatest elementJSONXMLUML
33:45
Source codeComputer fileSlide ruleMultiplication signFluid staticsCore dumpSequenceLine (geometry)DataflowPreconditionerSystem callOpen setException handlingCondition numberMathematical analysisError messageVariety (linguistics)Lecture/Conference
35:49
Connected space
36:40
Computer simulationComputer configurationCASE <Informatik>AutomatonDecision theoryProgrammschleifeCartesian coordinate systemNatural numberDependent and independent variablesMultiplication signLecture/Conference
38:32
State of matterRight angleOperator (mathematics)CASE <Informatik>Library (computing)Disk read-and-write headExecution unitVariancePresentation of a groupTheory of relativityMereologyMultiplication signParameter (computer programming)Universe (mathematics)TrailLevel (video gaming)Computer simulationError messageEqualiser (mathematics)NeuroinformatikReading (process)Lattice (group)Functional programmingDifferent (Kate Ryan album)Source codeCondition numberLatent heatCellular automatonOscillationProcedural programmingIterationSystem programming1 (number)ProgrammschleifeData managementStatement (computer science)Row (database)Matching (graph theory)InformationDecision theoryPreconditionerComputer animation
44:12
State of matterMultiplication signImplementationCondition numberFunctional programmingLatent heatConstraint (mathematics)DemosceneVariable (mathematics)SequencePreconditionerData modelTask (computing)Computer programmingCASE <Informatik>Parallel portMoment (mathematics)Error messageProcess (computing)Range (statistics)Electronic mailing listMereologyWave packetUniverse (mathematics)InformationObservational studyComputer animation
49:53
PreconditionerDataflowMathematicsMultiplication signMetropolitan area networkNumberProgramming languageCASE <Informatik>Level (video gaming)Goodness of fitEnumerated typeLine (geometry)InformationCondition numberTrailError messageCartesian coordinate systemState of matterSystem callFunctional programmingFerry CorstenCompiler2 (number)Design by contractLecture/ConferenceComputer animation
55:33
CASE <Informatik>SpacetimeWebsiteState of matterSource codeRepresentation (politics)Food energyMereologyVector spaceData conversionRecursionView (database)Context awarenessPresentation of a groupPoint (geometry)SoftwareExecution unitInterface (computing)outputCompilation albumSlide ruleInvariant (mathematics)Multiplication signResultantRevision controlPermutationImplementationComputer programmingRight angleAdditionPreconditionerStandard deviationData miningSound effectFunctional programmingProgramming languageProgrammer (hardware)Speech synthesisOnline helpArithmetic meanVarianceWave packetVideo gameWordSocial classUniverse (mathematics)Theory of relativityForcing (mathematics)Student's t-testInformationMusical ensembleLevel (video gaming)Lecture/Conference
Transcript: English(auto-generated)
00:08
So now we are scaling back the animations that we did in the previous talk on static
00:24
programming to use in 2012. I'll try to sort of form this as a tutorial. We'll start off with a little bit more of a common presentation that has an example provided by the day. I
00:43
didn't make up an example. I feel for the task, but I actually work on real code. But
01:02
programming is needed and stuff as well. Just so I sort of know, how many of you have not programmed in here at all? Okay, that's good to know. If you happen to hear either the previous talk this morning or the previous one? Okay, so how can you be more detailed
01:29
about it? Me, I'm an independent consultant. I'm mostly doing software development stuff, but also interesting things like inspecting cloud platforms and driving past the computer
01:48
games, studying finance. And well, since we have all heard about that much about data before, I'll just take some of the reasons why we should be using data. At
02:07
least the design on this way of seeing programming as a human security, about reliability, and about maintenance. Contracts, you know, that's mostly about the reliability and
02:25
maintenance. The contracts is a form of documentation which has the added benefit of actually being checked by the entire runtime or runtime, improving reliability
02:41
in that way. That's a very short story about ADEM. Then my presentation of ADEM is a single slide. It's not enough to learn the language, but you get an idea about it. It's a procedural programming language with support from object-oriented
03:01
programming. You're not forced to use object-oriented programming, but you can do it. There's what here people call modular programming. You can separate your project in packages, file packages. You have individual, standard, and such programs.
03:21
There's generics, which is an alternative to object-oriented programming called generalizing your solutions. And one thing that I like very much, and it's also very relevant about time management, that's the separation of declarations of such programs, the packages,
03:46
and the actual implementation of them. So first you specify the interface, and then separate from that, we write language implementation where you, just to make sure you're doing
04:01
the right thing, you have to repeat the basics of the specification again. And then as the program is distributed, you will have programming facilities built into the language, not just just add on languages, but actually as a part of the language
04:21
implementation itself. And then, like so, I actually want to distinguish my name rather than just by what values have to be possible to put into it. And it's composed of composite types, like the four classes, and our main program. And for simple types,
04:43
like various integer, code, and not very good types. And the most recent standard that was published, more or less, and maybe a lot less, in 1990. What is it? One hundred and ninety first grade, fifty percent up, in 2012.
05:13
But then, the 2012 standard is the only one in the series, and some of this,
05:21
which is new, which is exactly part of a base program. That's the ability to create those conditions for sub-programs, which is, as a minimum, the runtime checks, the state of parameters for sub-programs, before and after,
05:48
and then there's a type invariant and subtype predicates, which are the kinds of constraints which should be consistent for all objects in this time, at all times.
06:06
The differences between these three is the type invariants that are checks and private types, where you have, in the implementation details,
06:20
exactly which components is this type, where predicates that for, technically for subtypes, but for the type where you have visibility of the terminals, and they act more as constraints, and the difference between dynamic and static, that is related to how easy it is, basically,
06:50
to compile time and analyze the number. I have an example later on, where you'll see that the Python actually already, the connect TPO 2013 edition, kind of catch the compile time programming error,
07:10
in a case where the standard subtype predicates. Hopefully, in the future, we'll have more of the Spark 2 facilities migrating into the file,
07:24
so you'll have messages when you compile them. Well, your program will fail when you have to run it, and this line will probably end up fulfilling some condition, but we're not quite there yet, so we'll go back to Paris and work on it soon.
07:42
We do have the thing that people will say, oh, the component is supposed to load now. Well, yes, I know. So now, we still have to run various tools, besides the compiler, to get some of the checks and run time.
08:01
But besides all this new and fancy stuff, which data programmers make us perform time, there are also those times. We have the name, primitive times. If you have specific time, even if you have another type which have exactly the same values,
08:23
you can't just copy between objects over two times. You have to make explicit conversion. You have parameter passing directions on your subprogram, so you have to tell explicitly if an argument for a subprogram is parameter going in
08:44
or parameter going out, like one that's going to go in and then out, after so many pages. And then we have the rate checks on arrays. So you don't accidentally call the variables in,
09:04
measure, stop, sign, and array. And then we have sub-times, which is basically having an existing time, and then make a subset of it with ranges.
09:21
And then there are some cases where you have static checks, like that a case statement covers all the possible values of the argument for a case statement. You'll get a complaint and an error if you don't cover all the possible values.
09:40
And some of this is high-time checks, some of this is one-time checks. But it all helps catching errors earlier, and the earlier you catch the errors, the better. I've used high-times on a medium-sized project for the last year and a half.
10:09
And I must admit that even though we're using them, I'm not sure we've actually caught any errors directed by the pilot, saying he did something wrong. It must have been that way.
10:21
But it could be because we're good programmers. It could also be because we're not buying the contracts. That's one suggestion. So now I'm going to start going through each kind of contract element we have in Ada 2012.
10:41
I'll come up with some comments and a small example. To start with precondition and from the rationale for it, it's an obligation for all of us to ensure that something is in order
11:02
before you call the subprogram. And it's a guarantee for whoever implements the subprogram that this is true once you call. And I just came up with an example.
11:21
In Ada 2012, they hadn't actually put any of these contract aspects on much of the standard libraries. So I decided just to take some examples from the take my own API data. So we said we want to put a string to a context file. Well, we better make sure the file is open first.
11:43
So if this is one example, we can put in precondition. So in this case, we could, of course, have a recondition that, well, once we call it, it's okay. But the OS dismount the file system or make something else bring things.
12:00
Meanwhile, so the operation can still fail in this case. It's a nice minimal requirement. Similarly, we can look at preconditions, what we're saying after, so we're just calling the subprogram. That's an obligation and the increment of the subprogram
12:23
to make sure that this is true once the subprogram returns. And it's a promise and a call that this is how the world will be afterwards. And I decided that, okay, let's take the line
12:40
and the take my own API. And the data has, depending on your view, a nice or an allowing you to pass the feature of keeping track of line numbers in the file when you're writing to and reading from it. So actually, we can say that after you've done the line,
13:02
the line number has been incremented by one. So that's an example of a precondition. Here, I reference the value of the line number before calling with this acting old.
13:24
I'm sorry, 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, but there are lots of good references for that. That was pre and post conditions then.
13:43
Time invariance. This is an example I've adapted from the 2012 Ratchet Medal. Imagine you want to have we want to have the time able to represent
14:01
function that you need to use. I wasn't a mathematician once. We can start by just saying, well, we do it in rank vector angle at four minutes.
14:21
But then, the flow then can be anywhere. Then we give it some minus one to one. Then we get it into this box here. But we don't want it to end up on here. We can do that with an time invariant.
14:40
The distance from the cargo shouldn't go beyond one. So now we have a time here for managing points in the unit disk. Of course there could be any kind of condition here. But the point is that this is something that
15:02
compiler now is obliged to ensure objects of time disk on unit. That it always has to be true. You could actually, at this point,
15:25
derive from one that was just an arbitrary point where you'd say, okay, it can be anywhere as far as our building point time can represent. And then, this is a sub-time with sub-time constraints.
15:43
Then, the other kind of invariance that's dynamic sub-time predicates. That's the kind of constraints you stop setting.
16:01
Here's a nice little example here. A prime. It's an integer. It can't be less than two. You can't have any factors into the number
16:21
which are different from one and the number itself. Which, if we look at we're here saying that prime minus n is zero. That happens for some n from two up to prime minus one.
16:41
Then, it's not odd. The dynamic predicate is not true. So now we have a sub-time of integers which is only the primes. Unfortunately, we can't do fancy stuff by moving over a sub-time with dynamic predicates.
17:01
You can do that with you can do the static predicates with dynamic predicates. But you can at least make now you can just the lazy test now for which integers are primes is to just loop over all the integers and see if you can it's in the sub-time prime.
17:23
Of course, 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
17:40
could not be longer than 256 characters. And to avoid that we accidentally in our program tried to put larger longer strings into our database we made this sub-time where we put in a dynamic predicate and the length of these strings.
18:02
In older versions of data you could do something similar by creating a bounded string which could have length up to 256 characters. But all the work during that this is much easier.
18:22
And then I said before it was dynamic sub-time predicates. Static sub-time predicates are more limited basically it's the same but it's more limited expressions you're allowed to use. You can do anything where your sub-time
18:41
is in a statically defined set or part of an otherwise static expression. The sum 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.
19:03
And I was in Mauritius recently working for a small data company there. So I decided well we'll make a nice example the sum of it from November to April. That was the end of the window.
19:21
So now we have a type of month this is an example of operation types of data. And then I make a sub-type okay the sum of months from November to December from January to April. Then I declare an object
19:40
and then I accidentally switch back to Northern Hemisphere mode and say well July is the summer month. Trying that with a compile and you get the warning doesn't work. You get you get a failure because July is not the summer
20:01
sub-time. There's a similar example in the rational but it's written by an Englishman. He's clearly not used to the concept that the summer can go from November to April.
20:21
So he does it with a window from December to January. The effect is the same. And then I talk about coverage checks. Here I have a not very
20:40
nice example of a case statement. Level is if there's the level of some messages and then we say the different operations where to send the messages depending on the level
21:00
is split out in the case statement. But what would happen if I accidentally forgot to put in the level what would happen would be that the pilot would say that I'm not going to know the possible values of the title level and it would stop
21:21
my program and you have to go here and do something. It's not directly contracted but it's a very useful static implementation check. And it relates to the
21:41
sub-time of this value you put in. So that was a quick overview of contracts in beta 2012. Now it looks like it's seeing if I got everything included.
22:03
Okay. Then I've done my best to put some guidelines together to get a consistent use of contract-based programming in beta. When I started I just put things in and ran it on a sort of dev file. You can put something in here.
22:25
It's better if you do it consistently across the application of your library. the place I like to start when I'm programming that's with the types. So make sure
22:42
that you make good detailed declaration of the type and its constraints. You declare the type or sub-type depending on the requirement of compatibility without a time if you want to be able to pass it directly or if it should be really
23:00
a unique type that you should expect to copy back and forth. You can put appropriate constraints in your values. I had the example where the points where I put the constraint and the 30 point coordinate shouldn't be less than minus one or larger than one.
23:21
That's an example. And then you can add extra examples extra constraints if it is relevant as predicates or invariates in the type. I think you'll see that in many cases
23:40
you don't really need that. This is enough in the kind of a contract for the type. I go back to my integers in my prime example. It's nice. We start off with this prime integers.
24:01
And I decided here that well it's really an integer. It's not that special so it's just a sub-type of integer. If I thought it was really something special, I would say prime type prime this new integer and it would be a new type just definitely derived from integer type.
24:24
And then there's this about primes being larger than one I put the rate constraint on and primes are nice because that's not enough. We also need to keep track of the only factors is one and the prime itself.
24:46
So an example maybe I have to say so. I haven't used a degree of both. I did use Spark once to
25:02
validate applications to find primes. And I found an error I hadn't found in my testing. I was impatient. If I had tried to run to the end it would have failed around there because there was some mismatch running over the edge and the number of integers
25:21
in the process. It took some time to figure out it was that that Spark was telling me was wrong. It's definitely useful and it's useful in cases where you have to have the pages to find it by testing. I know also that the Spark people are being involved
25:41
in testing a cryptographic hash function where there's a part in the reference implementation if you give it two to the sixty-four five long data sets to hash and get some wrong value.
26:03
And nobody apparently had tested that. So the bomb is still there though it has been reported. But then back to the main story. Now we have to declare our types.
26:21
The next step is the sub-programs which are going to operate these types. I'm not going to introduce them on the sub-programs themselves, but when we know which ones we need make sure that we are as specific as possible about the arguments.
26:42
So we select the power direction of each argument. And we select the specific as possible sub-prime which are the arguments. And if we sometimes can't do enough
27:01
then we can continue to use pre-imposed conditions to declare use from those frames. My example here is a nice symbol and I'll probably be able to
27:21
figure out an example of increment, procedure increment counter. So well, the counter has to be incremented so it doesn't have to go in to modify and go out again. And we say we want to do it with arbitrary steps. So that's something that just has to go in.
27:42
And well it's both integers. Well actually counting, we start from zero there 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 data
28:02
by the way. So now we put some constraints here and the calendar and the step size. This is something you always need to do in Ada.
28:20
Some of the next steps here, that's well specific. Well, we put in a pre-condition since we're going to increment the counter can't already be the last possible value of our integers. And the first condition, one will definitely be
28:41
more than zero. Alright, but we can do better than that if we really want to. So we can go the step further and say we should have steps which will make the counter go beyond natural marks.
29:01
The other one isn't really a subset of this one but it's not. 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 algorithms. The next step
29:22
that's what are the requirements of our sub-programs? Which pre-conditions do we have? Are there any special requirements which should be in place before a sub-program? A sub-program will be called once in the whole run of the application. And it will only be called when the application
29:41
is in a specific state. And this is what we document the pre-conditions to the sub-program. Here, first I go back to the tech.io example where
30:01
writing to a file we have pre-conditions. The file should be open. But it should also be part of the writing system. So that would be an out file or any file, both. And another example that here I imagine I have
30:21
a variable function telling me about the state of the system. And initialize should be called if the system is non-initialized state. When I get to the working on an actual
30:41
time source example we'll have something like that to look at. Because there's a bug in the API that Digi has provided me with. That's good, I like that. Things to work on. Then
31:01
the next step is looking at likely sequences of course. So we have our types, we have our sub-programs functions and procedures. What are the likely sequences of course in these sub-programs? And specifically
31:22
with 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?
31:41
We want to call initialize as a precondition
32:02
that the system is initialized. And initialize doesn't have a post condition that the system is initialized. So that tells us how to figure out how to add post conditions.
32:21
We can see that it's a it wouldn't make sense
32:58
to say that the system is initialized
33:00
now. This is a case where Mark told us that we're not messing with
33:21
the initialization state. And shut down is not initialized. It might be not initialized allowing us to run and initialize again. So we could have things like that that are sorry
33:41
we could have splines also. That's a different example. Here we have another core sequence that's open file, fracture file. In writing, close the file eventually it will take more than one slide.
34:02
So we say the line has a precondition that the file should be open. That means that open could have a post condition that the file is open. And that makes sense. We want that. Actually
34:21
the way the world works is it might be open or it might raise an exception. There's more to the name error than we can get out of open. We didn't have enough lines here. So it has yes, we can call open and that's fine.
34:42
But actually in between we have to we have to be prepared either that we end up down in the exception handling set or do something else about the exception. But if the flow goes straight through the open
35:02
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 I'm not actually making up these sequences of lines likely sequences of calls.
35:22
Once you have the likely sequences of calls it's pretty trivial. Most of it is trivial. But still you have to do it. And then it's time for some source code I didn't write it myself so it's not
35:41
written quite for this purpose but rather for static analysis experiments.
36:41
This is a simulator of a sanitize experiment where you're running sand down from the top and it's falling down and the slope is too steep the sand will fall down either or it's simply not to one side
37:00
always to one side all cases it doesn't have to be a decision to come to one side or the other this is just to show the running application the main target of the session
37:28
so he starts his solar automaton and then there's a loop of updating and adding a brain next and then sharing and then
37:43
but what happens if we somehow forget to call the start of the automaton just commenting, but what we get
38:09
we get an access check which means that there's a finder somewhere inside this library that we're using which is null which is null and has not been
38:21
validated enough it is of course a way to stop another option could be that we actually make sure that we keep track of the stage of our simulator like this
38:41
and then we'll still get an exception, but it will be it will be it will be called if allowed in the system it will be called it will be called
39:02
when we go out the end of the loop really when we try to add a brain we'll know that we're not initializing so this in source it's a different base it's in microseconds of operations operations on the computer is not a big big difference
39:21
once we get the checking tools in place we run the smart verifier and it will make a difference then we'll get a downtime check the preconditions don't match up so what I was planning to do was I just as a demonstration go in and put in
39:42
some stage management right I think is here in this library and to show you that we get well what we get now is not a downtime error but we get a different error
40:17
it's big enough that everybody can read right
40:21
and it's still big enough that everybody can read also in the back row so this is the specification the external specification cellular oscillator simulator it sets up a lattice
40:41
that we're operating on it has a kind of source where we're putting in sand and some parameters shading the decisions part here and then we have
41:02
the actual operations starting and stopping adding the grain going to the next step in the iteration and showing that it's there but without any preimposed conditions
41:21
so what we could do is we could I would start to say we could try to try describing the state of the automation and what could be uninitialized it can be
41:45
switching this is just the type the kinds of states we say
42:01
I cheated and looked inside it and as far as I can see after we've started up again that's why I don't have a separate state for being uninitialized beforehand after having started again then we want to be
42:20
able to check and ask about the state so we specify a function that returns an automation state
42:42
so now we actually have enough information out here that we can start to add post conditions first things of our operations we could be the problem so you say well there's no parameters
43:01
so there's nothing that can all work so we say we start our start procedure has a post condition which is that it is initialized state equal initialized state equal initialized yes, exactly
43:25
somebody remembers and starting similarly
43:43
and the other ones they don't change anything so this is what we have my first statement what are the post conditions so going back to
44:00
that's because I say what do we do I'm not doing it right because really what we should say
44:20
is that what do we need no you didn't call all the errors literally no yes then adding a range you can only do that we saw we got the constraint error
44:42
we have the pre condition then we are initializing the state the same as the case for next I showed we have to initialize how complete are we
45:09
now the what we do is we say start and then we say
45:20
have rain then we say next then we may say show and then we may go back here sometimes and then sometimes we say start and pre conditions
45:41
here like this the start actually tends to deallocate and if it tries to do that we better be
46:02
it's good to be uninitialized because otherwise I know there will be a memory and if some of you are wondering
46:22
why I'm putting the switching state in between it's because behind the scenes there's actually a task in it it's a parallel processing program so in case some function somewhere might be asking
46:41
why we are changing the states I suppose we better have the possibility to say which switching state at the moment which means that I really have to make the variable the state should probably be atomic we could just
47:05
put that variable in here notice this the package specification is separated in the public path which is the one that
47:21
the users of the package can see and the private path which focuses on details about the data modeling
47:42
but you can also do certain variables in the private path instead of improving them all the way to implementation
48:05
ten minutes left actually five minutes if you allow time for questions we should have at least time for questions then you should tell them so
48:24
because we're here what did we say we said keeping the state well we didn't initialize the path
48:41
but before we said it should be uninitialized and we said
49:25
adding a brain next to show as preconditions are being initialized that's good and we're putting in what we have so
49:41
start after we call start we are initialized and after we call start we are initialized for this sequence we have the precondition of add is included in the precondition
50:00
of start that's fine next as precondition is not included in the precondition yet it would have it would have control data flow it wouldn't be a problem because we know that it doesn't change the state but we're better here go in and say well
50:22
actually the first condition of add we're still initialized just to make sure that we don't get problems next to
50:51
in this function here
51:06
giving us those main states and what we do
51:46
is an assertion failure
52:04
which basically means that one of our contracts were wrong and it says it is faulty anybody who kept track enough that they were able to tell us which one that is
52:24
so add a brain fails I'm surprised because you removed the initialization you're not changing the value you're never changing the state
52:42
yes, what surprises me is that I had expected the post condition of start to be the one that failed but you never call start you removed the call I removed that call that's why so maybe we should go in
53:01
so we get the line error yes, so we go in and activate start and something that blocks out
53:35
where did you go? are there any race conditions in your applications again?
53:40
yes, sir ok, first so now we get an assertion failure but if the compiler works we know we should get an assertion failure at exiting
54:00
the information start so now we go in and say now we talk about the state we'll actually go in I'm asking you to stop by pressing
54:42
Q, we will enter stop and stop will start fine but on exit we have not said I'm initialized then we should get an assertion error failing post condition line 37
55:00
yes so we can see that we can work, we can play around with these clean post conditions and we still have a few seconds I'll go and notice
55:21
so I'll I'll stop now bad style in in Ada you can declare enumerated types as I did for the automation state so a case like this you really make a state type which is
55:41
empty settled and then you find obvious representation a way to the characters also making sure that you set the empty issue space settled but that's it
56:01
and then not so much but most of our things are set and you can find source code examples here my website there and I'll put my slides on my website
56:20
all the slides I'll publish mine in a few minutes now I know how they are connected any questions? any which are short enough I was just wondering about this example with the with an invariant that guarantees that
56:41
a point is on a unit I was wondering whether when is this check actually enforced and how will that impact performance or whether I can even use such a well complicated let's say invariant in practice it is enforced
57:01
let's see sub-program sub-program type conversion it's basically enforced each time you access the interface
57:20
which is anytime you have it's time to do something which could change it right type conversion type conversion and returning from sub-program one that has a return value if it's just an in nothing will be done
57:40
but yes it might impact performance my view is I prefer a slightly slower program which gives me a correct result one that gives me an incorrect result if I want one that gives me an incorrect result I can do it pretty quickly anyway
58:02
I'm sorry I missed the beginning of your speech but I'm an effect programmer so we have you had stuff like this for a long time one of the issues in the in the in the in the
58:20
in the of the it is resolved I can't remember the details and I'm not one of the people who have to implement iOS Jose can you remember the details about the standard
58:41
results issue? I'm pretty sure I've seen something exactly about how to resolve that issue but I can't remember the details
59:03
I'm sorry I can't help you with the details I wouldn't mind trying to figure it out thank you I think the program you mentioned is when you have something like stack full with a precondition not stack empty
59:21
and stack empty with a precondition not stack full that's right and in ISO if I remember correctly accessions are disabled while you are checking another accession yes, and permutations differs
59:41
depending on compilers it arrives when for example you say ok my result is not the result of the function that is prefixed with not well that's what I said people are not full empty implies not full and full implies
01:00:01
Not empty. I remember we discussed that during the design of the language. I can assure you that there is nothing like disabling in certain contexts.
01:00:22
Now, how will you solve that one? I mentioned this morning that the reference manual is freely available. Also, you have an HTML version of that. And you have another one, which is called the annotated
01:00:43
reference manual. And in addition to the nomadic text, you have comments that explain the rationale, the decisions, and the things that have been discussed when designing the standard.
01:01:02
So in a case like that, the best thing is to refer to the annotated reference manual. There is certainly something about that. Liz, it doesn't say recursive. Reversing is what it is here. Yeah, but do you have the annotated manual? I haven't got the annotated installed, no.
01:01:22
I could, of course, activate the network. Just type annotated in the reference manual. Yeah, but I turned on the network, so I wasn't distracted while presenting. Well, maybe you can take that offline. I think we should do that online, because we have another presentation coming up now.
01:01:42
Let's look it up. And thank you. So the next presentation is about the annotated reference manual.