Player is loading...

Embed

Embed code

Transcriptions

Note: this content has been automatically generated.
00:00:00
but
00:00:02
well thank you all for coming and it's five pleasure to and to
00:00:06
talk to about using formal methods and i'm going to concentrate on
00:00:11
uh how you get started with what formal methods and some of the things that um
00:00:15
that you can apply for so um it's only fair to start off by saying what what are formal methods
00:00:22
a formal methods are a mathematically based or logically based
00:00:27
approach to uh to writing software and by writing software i mean
00:00:32
writing specifications that say what the software supposed to do a writing the code that's actually going to
00:00:38
to execute on the machine and then trying to connect those two pieces in in some sort
00:00:43
of way that is that through verification to check that the code is really doing what what
00:00:47
the specifications are telling us that the uh what we intend for the software to do
00:00:53
so it's um it's also good to explain the various words i had on my
00:00:58
longs title slide so formal methods was one and young software engineers was another
00:01:04
so what are young software engineers today well they're probably
00:01:08
engineers software engineers were just starting college maybe
00:01:11
i'm maybe they've gotten started in college maybe there are few years um until they start college
00:01:18
how can these people be um be getting exposed to formal methods so that they can use it in fact
00:01:25
is as they're developing software um and in industry or for uh for any other purpose so um
00:01:34
um formal methods are mathematically based that is logically based or they are precise
00:01:40
in some ways but why is that something that we would like
00:01:44
well there are a fair number of of of considerations
00:01:47
in software uh production today and one is correctness
00:01:52
when you when you write the program you um you would like to to make sure that doesn't crash that
00:01:58
is perhaps one of the one of the first things that you would think about software uh and um
00:02:03
in the um but twenty years ago we started
00:02:06
seeing in the press affecting serve everyone's lives
00:02:10
various is a source of um security attacks uh there were typically at that point um
00:02:17
it came through buffer overruns a buffer over on is just
00:02:21
uh your computer accessing memory word word shouldn't be so these
00:02:25
are program errors that allow certain kinds of security attacks
00:02:29
so memory safety is something that we would like well memory safety is something
00:02:33
that you can obtain if you start using the language that um
00:02:39
that is type safe that does not allow you to access any part of of memory like for example
00:02:44
c. program but there are other other things that you would consider as well you have um
00:02:50
you have run time exceptions so if you run a java program for example
00:02:55
um the program may it may all the sudden and because you've uh you've attempted some operation that was not allowed
00:03:02
so the good thing with that is that as the program and
00:03:06
setup point you're not uh you're not inviting further security attacks
00:03:11
but uh but having such problems in your software means that your your customers
00:03:16
are going to be um a bit worried by by this behaviour
00:03:20
and perhaps customers go to different uh different platform different application
00:03:25
and stop using stop using your apps stop using your web sites uh
00:03:29
they don't trust you anymore they they want to do something different
00:03:32
but it's also costly to and to fix these things later now
00:03:38
if it's yes is a crash you can't fix them by um
00:03:42
by reporting by collecting various kinds of uh a crash reports
00:03:47
that various apps and um and the software programs would report
00:03:51
back to you so because of the the software deployment
00:03:55
that process today you can get these things out to customers rather quickly for example if you have
00:04:02
uh if your um if errors are on the on the website you can just update your software on
00:04:07
the website you don't need to update that millions of apps all um all of the world
00:04:13
but then there's one more step which is that of functional correctness so why would you want to go all
00:04:19
the way to functional correctness to make sure that that your program is correct well sometimes you don't
00:04:25
some programs it's okay if they don't if they don't always work
00:04:29
um and wise that well there's lots of priorities uh
00:04:33
you um you may want to release the product just as quickly as you can um you may want to um
00:04:40
um to spend less money because you want to see that you are these
00:04:44
the features that the customers would want to have in the first place
00:04:47
no that's um these are strategies that's some uh some groups
00:04:51
and software companies uh it may choose to to apply
00:04:55
so i would not expect in the future that all software is going to be verified
00:04:59
to be functionally correct but there are places where functional correct this really matters
00:05:05
no one place where you would like to go beyond just the
00:05:08
the simple crashed for unison programs is the area of security
00:05:13
and when you when you deal with security there is no such thing
00:05:16
as as having a program that is just partially secure that's
00:05:20
it's not going to be just a little bit secure it's either secure or does and uh if it if it
00:05:25
has folder abilities that attackers can uh can make use of
00:05:29
then your data um uh is is not safe so
00:05:34
putting a price at obtaining security is something that um
00:05:38
uh that you may want to do that that is if you um if you have a resource budget for
00:05:44
for your programmers for your software engineers putting effort into making sure
00:05:49
that things are secure uh is a good thing and um
00:05:53
so security is that is a really difficult thing even for experts and um if you have all of
00:05:59
the the literature in the last uh twenty thirty years you will found a a number of
00:06:05
uh problems in uh and encrypted graphic protocol sort of number breakage is
00:06:10
and uh so even with the experts these are difficult things
00:06:13
to do but if you're if you're an amateur just getting used to things then uh then you probably shouldn't attempt it
00:06:20
but if you do you see i'm paying a special attention to all of all areas of correctness is is really key
00:06:26
you know these are things that that you may see if you're
00:06:31
if you're going to develop programs in uh in and say i'm in a company setting
00:06:35
uh you have some products that you're that you're putting out there but what about
00:06:39
what about all the rest of us who are writing software in in various other ways that perhaps are not
00:06:44
as important we think well you still need you still need to think about getting a program correct
00:06:50
even if your program is not the highly the most highly critical software
00:06:55
that that you're producing you still need to have some mindset
00:06:59
uh some uh some techniques everything about your program that lets you figure out
00:07:05
is this program really going to work or not but it's it's it's not okay to just
00:07:09
had various statements the program and then hope that one day perhaps it is going to
00:07:13
be cracked you need to actually think about what these things are just like
00:07:17
other kinds of engineers would have various methods of calculating if we're
00:07:22
bridges gonna stand up and and so forth there are methodology
00:07:25
sinner techniques in software engineering that let you think about programs to make sure that they that they really are okay
00:07:31
and the good thing here is that there's plenty of tools support today um there wasn't a tool support
00:07:37
for these things say twenty twenty five years ago a lot of things have happened since then
00:07:42
and um so you can get a lot of help and that help can be their balls for
00:07:46
teaching people about how to how to reason about software and also using it in fact this
00:07:52
okay so i'm in the future the new software engineers the young software engineers of today
00:07:59
uh or a likely to see these sort of uh the first a crack this insecurity issues a lot more
00:08:05
um the um with data being stored uh even more so when in the cloud
00:08:10
uh you worry about security and making sure that that everything is um
00:08:14
uh is kept safe uh and um and the tools can help with that
00:08:19
so um what about the cost if you mean it would be really great to be able to have a ball that that says
00:08:26
using formal methods is going to make your software development keeper is going to let you
00:08:31
get there faster is going to let you compete better as well um then
00:08:39
many of us would have that feeling that we can get there but if you look at measurements i think
00:08:44
there's only one project that really has a lot of these measurements and jim uh mention this project project
00:08:50
it's the s. c. l. for project in them from australia
00:08:54
which build a um a a micro kernel and um
00:08:59
uh that colonel has um when it started it was about ten
00:09:04
thousand lines just under ten thousand lines of of c. code
00:09:07
which is not a lot of code it's something that you could you would think are sure i can write that in a weekend
00:09:12
but uh can you write it correctly the question and to begin with uh
00:09:17
they had about two hundred thousand lines of specifications and prove scripts
00:09:24
so that is about twenty times the the number of lines of executable
00:09:29
code well today that number is is even higher because because
00:09:33
this group has has had a lot of things so in fact i think that these numbers a little bit outdated even so
00:09:39
but the but you can see that there's a large ratio here of lots of
00:09:43
lines of specifications and prove steps to the number of of lines of code
00:09:49
so now you might say cheese this what i'm in for well that one thing is that we're all
00:09:54
learning how to do these sorts of things and uh they have had a particular tool set here
00:09:59
they have a dealt with a number of especially tricky problems but they've also done
00:10:05
measurements over these many years and i think that this group has done
00:10:09
that these measurements uh breast but it's actually no one else has and what they have shown that compared
00:10:15
to other less packed this is approaches that even with these numbers that you may think are
00:10:19
our um extremely um large of of a large gap between the ten thousand
00:10:25
in the five hundred thousand lines of of uh specs improves is that
00:10:30
compared to other that's packed this as they found that they're only somewhere between a factor
00:10:34
of two and three away from the cost of developing something similar you saying
00:10:39
uh other best back this is like a testing and and things like that and of course when
00:10:43
you write test suites those add up to a lot of lines of code as well so
00:10:49
if you believe these numbers are representative and if you believe that we can do better
00:10:53
than the the ratio of well as i'm showing here fifty fifty two to one
00:10:59
uh if we could do to improve that ratio only to by a factor of two or three
00:11:04
then maybe we couldn't set here and make the the argument that is always going to
00:11:08
be caught more cost effective for these sorts of projects to to apply formal methods
00:11:13
so you know the case it's showing that when you when you
00:11:18
strive for tools uh correctness when you want to make
00:11:21
sure that things really are correct and secure there are techniques that can help you get in in in that direction
00:11:28
okay so there are pieces of code that you would like
00:11:32
even today uh let's say you're writing a variation of
00:11:36
binary binary so a binary search and instead of i'm wanting to find
00:11:41
exact elements the exact index where something is you want to find
00:11:45
the place where you want to insert something if it isn't actually in the in the right that's like
00:11:50
so maybe have or a library routine for doing this or maybe you're gonna write it yourself your writings such
00:11:56
a routine yourself and you could imagine a lot of other routines that you would write of this work
00:12:00
there is no reason for you to to have any errors in this code at all
00:12:05
would you probably want to do is you're gonna test it a few times if you're good software engineer you
00:12:10
will write um a test suite that you that you incorporate with them with every building every every change
00:12:15
but you can do even better than that have not too much cost if you understand
00:12:19
what these methods are now i'll show you some of of that as well
00:12:24
and um the formal methods as i mentioned before just that
00:12:27
the reasoning process itself the thinking process that goes on
00:12:31
uh that when you use formal methods is um is going to help you be be a better software dinner
00:12:37
so well how is it on there are three areas would be may think about here um verification specification and development
00:12:44
i had these on in a different word or uh in that we're not defined formal methods on the previous slide them good putting them
00:12:51
in this war because i think that this is perhaps how most people think of of things they might think of verification first
00:12:59
well i have some piece of code i'd like to make sure that it's correct how can
00:13:02
i make sure it's correct well i'm i might wish for just the push button tool
00:13:07
another or in such areas where uh being able to run the pushbutton two
00:13:13
or maybe running it tool but some specification that some expert road
00:13:17
um and it one example of this is the uh the slam project that
00:13:21
took place um in fact in them a gym there's group and um
00:13:27
when norm well almost twenty years ago now at uh at microsoft and uh this is the kind of a pushbutton
00:13:33
technique where you could have a a tool that uh that tries to find yours in a program for you
00:13:39
but if you want to extend this to your all sorts of things outside a particular domain
00:13:45
chances are that you were going to have to interact with the with the verify or
00:13:49
and i claim that this is a really good thing because uh if we never interact with the verify or how are we going
00:13:55
to get any thinking help from the verify or we would like to the tool support that we have to help us think
00:14:02
and if we never interact with that if it just says yes or no when the and
00:14:06
uh then how are we going to to be able to to think better because of the tool
00:14:11
so um we like things to be as automatic it as possible but when there's a net
00:14:16
interactivity i think that is that is can be used as a really good thing
00:14:21
so that's a verification side of things but really there are many other parts of formal methods that that help you a lot too
00:14:28
specifications is one that some people would think of specifications as being
00:14:32
the thing that you do will formal methods and maybe never
00:14:35
connected with code because the specifications help you abstract
00:14:40
and help you model things and help you think about what is it that these that that my software is really supposed to do
00:14:46
and as we all know this sooner in the development process you
00:14:50
can detect errors and a fatal flaws of your your architecture
00:14:54
or what you're trying to do the the cheaper just to to change gears and do something that is going to work
00:15:01
so writing specifications is a really good thing when you when you write the
00:15:05
specification for let's say class or module in whatever language you have
00:15:10
if you can think of how to write that specification in a way that the that you expected
00:15:14
all callers will be able to read the statement of of what's going on and understand it
00:15:20
that probably means that you had exposed enough of the abstraction to your callers and that is a really good thing
00:15:26
um you might find when you're writing specifications that all they're probably some hidden states in here that i need to tell
00:15:33
all the clients of of the class or the model about those things can come out when you're writing specifications themselves
00:15:40
and then in the development um that is something that that a number
00:15:45
researchers have had as a goal that's formal methods are used
00:15:48
in development that you write specifications and somehow you automatically you push a button and you
00:15:54
synthesise the code or you um you do some hand holding with the um
00:16:00
hand guidance of the the tool and and eventually you get the software well
00:16:04
that's that's something that can work in some domains but as of
00:16:08
try to emphasise several times using that using the formal methods themselves the reasoning
00:16:12
techniques as the thinking tool is something that is going to help you
00:16:17
okay so i'd like to just mention this if you milestones um and that there there's so
00:16:23
many so i mean i'm just going to mention three little things and they will
00:16:27
a support little bit what i'm i'm what i'm talking about that are there so
00:16:30
many other um that i'm leaving else it's it's not like this is a
00:16:35
complete history of of things but um if you look in uh the early seventies
00:16:40
in fact things started really in the in the early sixties where um
00:16:44
we're um many people started thinking about the correctness of software and and um how can you
00:16:50
what sort of mathematical techniques could you have and so twenty four
00:16:54
published the program in nineteen seventy one there were some similar programs that were being written as well
00:17:00
and um these programs had specifications in them uh this is i'm using really small fancier
00:17:08
but the um um but the program that you published has invariance it has
00:17:13
preconditions it has supporting arguments for why this piece of code is correct that is
00:17:18
it has stuff in it that the compiler is not going to use
00:17:22
and that's a big step for for any software engineer to take the step of saying i'm going to supply things
00:17:28
uh in my program text that is more than is needed by the compiler that's a step
00:17:32
that you must take a before you um can read any of the other benefits
00:17:38
so now uh a lot of people dreamt about these things in the
00:17:41
in the nineteen seventies and the mechanical tools that existed at
00:17:44
that time were just not there to support the the full vision of of what people expected to be able to do
00:17:52
in the mid eighties another milestone is bertram myers uh that i
00:17:56
fall programming language so i've full balls use object around orientation
00:18:01
which was um uh was ramping up and um and also put
00:18:06
what he called a contractor design by contract into the language
00:18:10
no this is not the first language that had contracts in that but this is really a piece that i think a popular rice this
00:18:16
idea and and made it into the whole language into the whole language
00:18:19
designed to have things like p. impose conditions in the language
00:18:23
so they're not the foreign part that you're trying to add later but you have it there
00:18:27
as your writings saw for the first place and that makes a big difference um
00:18:33
then in the um in the mid to late nineties
00:18:37
um java started becoming a quite popular and if you look
00:18:43
at how java as a job as libraries were were
00:18:46
designed at that point how they were documented you could see that that there were hints of specifications in them
00:18:54
and there was a there was a mindset that you should try to get your programs to fail as quickly as possible
00:19:00
that is both with the run time checks that the language itself imposes but also in
00:19:05
the the specifications that you would uh that you would write down or imagined for
00:19:09
for the software that for the libraries you'd like to have things fail as
00:19:13
quickly as possible because in that case you could find errors more quickly
00:19:17
i'll show you another on on another slide an example of this and
00:19:21
around this time the java modelling language uh which here elevens
00:19:26
that pioneered and and designed um from the help of a lot of different people
00:19:31
uh became a specification language um for for java in particular and
00:19:35
that sort of subsumed uh a lot of other such efforts
00:19:38
and serve incorporated them into into gem elsevier was one standard way
00:19:42
to write a formal methods for for java like programs
00:19:47
okay so here's a um yourself um
00:19:52
a one page where part of page from the specification the java that you till vector um
00:19:58
class and it's the insert element aftermath that doesn't really matter so much
00:20:02
but it is the highlighted some things in in yellow here
00:20:06
in the text itself it says something about the parameter called index
00:20:11
and it says the index that must be somewhere between zero role and the size the current size of the vector
00:20:17
now that's something that you might write in a in a piece of documentation well this is something that you can also form license some sort of way
00:20:23
the way that this was done in java was that a job would check these um these
00:20:30
sorts of preconditions i call the preconditions they would call them parameter about validation is probably
00:20:36
and it's as as you can see here it's as if the index is less than zero or if the index is
00:20:41
greater than the size then this description of the methods tells you that you're going to get some exception back
00:20:49
now what i interpret that i interpreted that that as a precondition i should
00:20:53
not be doing this that is i should make sure that i
00:20:55
don't get this exception i should make sure that i that i pass in in an index that is um that is within range
00:21:02
so the good thing with this is that that the specifications were riding yeah were written down so that you could always read them and
00:21:09
see what they were uh even though they were for for parameter
00:21:12
validation which is just a small small part of of preconditions
00:21:17
but it also helped uh the young software engineers at that time
00:21:22
because as a software engineer when you look at these um as at this documentation this a. p. i. documentation
00:21:28
that that describes what interfaces doing you can um you can see the style in which it's written
00:21:35
and so other java code would also start doing these uh fail fast
00:21:40
uh kind of paths that is we would thrown exception if if
00:21:44
the parameter values were not what you expected and this is one of the things i expect to happen with formal methods as well
00:21:51
that is when you see formal methods being used if it is in place in such a
00:21:56
way that the young software engineer can see them for example in documentation when tool tips
00:22:03
or in some programming language that uh that becomes popular so that it there are there
00:22:08
used then uh that i think that the software engineers will pick these techniques up
00:22:13
i don't think that there's anything um that's stopping them for example that that it's too hard to think about
00:22:18
or it's just a matter of of habit so getting this the young software engineer into these things
00:22:24
uh is one thing that we can do by by placing them visibly um
00:22:28
in documentation and as i said tool tips other things in the languages
00:22:33
okay so let me go through um three things from formal methods preconditions pose conditions and
00:22:41
the variance and then i'll put these together just to show you the flavour of
00:22:45
of how i see these tools being used for uh for software during
00:22:50
so let me start would preconditions the precondition for a method where routine or procedure um
00:22:58
is is a condition that you expect to hold when that method is called
00:23:03
so now the question is alright so if it's expected to hold
00:23:07
when it's called who is supposed to establish this condition
00:23:10
for precondition is always the caller that is expected to establish the precondition
00:23:16
and then the inside implementation you could just assume that this condition holes
00:23:20
that's is but a precondition is and i think that preconditions are the most
00:23:24
important kind of specification that you have anywhere if we could teach our
00:23:29
computer science students um to come out with their degrees and they
00:23:34
all know of very well exactly with the precondition s.
00:23:37
and they can write down the precondition i think we would be in a much better situation with writing software than we are today
00:23:43
and that seems like a small thing um the having a precondition means that we divide up
00:23:48
the the responsibilities who's going to check these conditions to make sure they that they hold
00:23:53
if they're not mentioned in the preconditions then maybe it's something that implementation is supposed
00:23:58
to be checking it and uh having preconditions another specifications they hardened all
00:24:03
the interfaces which means uh that that we take on this sort of fail
00:24:07
fast mentality if you will that is we say what supposed to hold
00:24:11
that is when you run your test suites you you can check not
00:24:14
only that the final result of running your entire program is correct
00:24:18
but you can check that the execution all all all along the way was what you expected it to be
00:24:25
so what is my advice here well i'm my advice to a
00:24:28
young software engineer would be start with parameter to validation
00:24:32
if you start with parameter validation you can get a feel for what our preconditions and these are really important things
00:24:38
to getting the parameter validation in your program if it's um if you if you throw an exception that's one
00:24:45
way of doing it here i'm showing one line from the dot net a coat contracts which is um
00:24:51
the way that you in your programming language uh in this case c. sharp can just include a run time checks
00:24:57
for these are the sorts of things so this is one way for for the software here to get started
00:25:03
okay post conditions well they are sort of the the the dual of the preconditions
00:25:07
they tell you what is expected to hold at the end of a of
00:25:11
a procedure body a word at the end of the method body
00:25:15
and the the the um the dual also holes that it's the
00:25:19
implementation that is supposed to to establish these things and
00:25:22
that means that the caller can assume these things after the call and that's a that's a very nice thing
00:25:29
um if you want to go all the way to specify functional correct this you need post conditions
00:25:34
but if you're just getting started chances are that you're just gonna stick with preconditions for awhile preconditions are
00:25:40
or more useful to get started with everywhere um but if you want to go all the
00:25:45
way to functional correctness the post conditions are going to say a lot of different things
00:25:49
um there are also a lot of things in a p. ice if you if you look at them
00:25:53
that maybe just incidental that the people start relying on that is made it so happens that
00:26:00
the routine might in some cases return a negative value well maybe you detect that it looks like
00:26:05
it's always returning minus one and maybe in your code you start comparing with minus one
00:26:10
well that may be a bad idea because maybe maybe you can get the different negative number
00:26:16
in in other cases so having a specification that states what that contract
00:26:21
is between the cauldron call the it's a really good thing
00:26:24
so my advice here is that if you're young software engineer and
00:26:28
you start fighting pose conditions doled go crazy with them
00:26:33
what i mean by that is it's really easy to try to move up your ambitions to
00:26:39
try to bite post conditions that are very elaborate imagine having routine that is going to
00:26:46
put a dialogue on the screen well what is that was the pose commissioner that
00:26:50
well that you have something else on the screen that serve me make
00:26:54
some button that says okay and so forth and you could try
00:26:57
to write these things don't do that um try to rights much
00:27:01
smaller pose conditions and ride larger ones as the need arises
00:27:06
um that's going to keep you say is also going to keep you
00:27:10
locked into a good engineering position which is the um finding
00:27:15
divide trade off between um between the routers that you're getting on your investment on your last time
00:27:23
okay so the third thing is invariance so invariance um our conditions that hold always
00:27:32
well they don't always all day the whole at important times
00:27:37
for example maybe if you're in an object oriented setting they hold whatever no one is operating in
00:27:43
on the object that is when the whole method is executing the object at that point stable
00:27:48
uh if you're in um concurrent setting and you you use something like monitors
00:27:53
yeah that is locked that protects some data that the monitor invariant is
00:27:57
something that holds when no one is operating on that data
00:28:00
so um so the very into something that holds always or at least at certain points under
00:28:07
many different kinds of invariance um system invariance a
00:28:10
monitor variance loop invariance data structure variance
00:28:15
and these invariance are mainly for the implement or um that is when you
00:28:20
implement the data structure you won't have it clear in your head
00:28:24
what you what you want things to uh to be to be um for the representation of what you're trying to do
00:28:30
so what is my advice here well i'm at mit uh and
00:28:35
i think this came out of the the clue days
00:28:38
um the with the the clue programming language a barbell this coven don't go to again and many others um
00:28:45
there was um you would write a rat okay method so replicate method is something
00:28:50
that's just want to check that your data structure isn't a good shape
00:28:54
that is that the representation is in an okay state and then if you write
00:28:59
such a method you can then call this method anytime that you like
00:29:03
and this is one way to checked invariance you're writing down invariant essentially in your
00:29:07
replicate method and then you're calling it when you wanted to to hold
00:29:11
um so if you're trying to learn to do to do verification using invariance then there's a concept called
00:29:18
an interactive invariance which means that invariant needs to say enough things so that you can prove six
00:29:24
and this is similar to if you have a if you're doing mathematics and you want an induction hypothesis sometimes we know that
00:29:31
you need to strengthen that induction hypothesis to be able to prove what what you
00:29:34
want to prove so to learn that there i would i would recommend
00:29:39
uh starting off polluted areas because they will show you that they've just sort of things that you need to know about uh verifying
00:29:45
things with the variance okay so what i want to do now is i'm going to show you these things at work
00:29:52
and so we'll do an example and um as i was riding through the uh the swiss landscape
00:29:59
yes ray by train uh i was thinking ah let's do the saddle back search
00:30:04
example so um so um this is going to be one example but i can show you
00:30:10
some preconditions post conditions and any variance and um let me explain what the problem is
00:30:16
so in saddle back search you have a you're given a two dimensional array
00:30:22
uh something like this and that we're going to search for an element somewhere in this right that's why it's in that buys the search
00:30:29
but it's called the saddle back because we're given a some properties about this right
00:30:35
we're given that the values if you go up the uh um if you take a
00:30:39
particular point in the x. axis and you go up the the y. axes
00:30:43
things and roll monotonically that is they they keep on growing as you as you go up
00:30:49
it's also the case that that the holes in the other direction so we're given that the over the matrix
00:30:55
the rated two dimensional array that were given has these properties that values role when these these directions
00:31:01
so what does it mean now to find an element so we're gonna
00:31:05
find an element as somewhere in the uh uh in this matrix
00:31:09
so the typical thing would be that you would start at let's say the origin
00:31:14
there we have it and you would you would search for the element and you could
00:31:18
imagine that the search would go something like that then ooh we found that um
00:31:23
so uh that's something that you that you might think of operationally but what does this
00:31:28
mean in terms of invariant what is the invariant of such such a thing
00:31:32
well it is that we have some area of the matrix that we have still to explore
00:31:39
that is as we go on their certain parts of the matrix that we um that we don't need to look at anymore
00:31:45
so let's say that we are given that the element upper looking for it does exist
00:31:49
somewhere in the in the matrix in that case uh and show in animation here
00:31:54
the as we do the search were blocking off certain parts of the
00:31:59
of the matrix that we no longer need to look at
00:32:02
so the invariant in this case is that the white area is
00:32:08
the button white area contains the element that we're looking for that is the marriott
00:32:13
so if we want to move the yellow circle that is the current
00:32:18
position if we want to move that somewhere uh in this
00:32:21
way that the way i did it if you want to move it to the right then you may get better make sure
00:32:25
that the elements we're looking for is nowhere to the left of what we're removing the point too
00:32:32
that is unlikely
00:32:36
density p. yet so that's alright so well it turns out that if you're going to do saddle back search there's
00:32:44
a moment of creativity that you that you need and i'm going to show you that moment now and then
00:32:50
after that moment of creativity everything is actually just simple um at the moment of creative give it that you
00:32:56
need to what you need to realise is that the way that i showed it on the slide
00:32:59
it's it's not a good technique for getting there um would you like to do is the following
00:33:05
uh you realise that this model tenacity well it's sort of like the
00:33:09
them the money in the city the values flow up words
00:33:12
in this direction and what does this remind you of
00:33:16
in switzerland well of course uh the beautiful landscape and hills and so forth
00:33:23
and uh so here i'm trying to depict that these arrows go up in the direction of the elevations as you move
00:33:29
around in this matrix um we're getting higher and higher if
00:33:33
you go uh up in the extraction worldwide direction
00:33:37
alright so uh well now what well now we can think of the contour
00:33:41
lines and the contour lines of this landscape look something like this
00:33:46
and it turns out that now if we want to find something in this
00:33:49
array one way to do it is that we start not that the
00:33:53
origin but we start at one of the diagonals we can start in
00:33:56
the upper left hand corner or in the lower right hand corner
00:34:01
um so um so if we do that then we can move this point
00:34:04
around and we have the same kind of invariant as we did
00:34:08
before in that were blocking things off to um that were saying
00:34:13
in those blue blue reaches we no longer have to log
00:34:16
and this is uh this next to program a bold doable at all and it also makes for nice invariant
00:34:22
okay so i hope that by this um animation that i've shown you what invariant is supposed to be so
00:34:29
now all we have to do is is right the code like so um we will do that
00:34:36
so i will write the code in um in a language called daphne so daphne was uh
00:34:43
does is the programming language that is designed for reasoning so
00:34:47
it was designed to make it possible for you to
00:34:50
uh to balls incorporate specifications into into the programs but also have
00:34:54
the verify around uh as you as you go along
00:34:58
alright so i'm going to write the um uh sell back search
00:35:02
and uh let's evaluate how is a um a um
00:35:10
how's that font sizes the museum and that's alright
00:35:17
okay so all of the um the method is um takes and takes in an array
00:35:24
that we had discussed and it's going to return to sex is going to return
00:35:27
uh the place the the coordinate m. and where we're going to find that that's this flag
00:35:33
uh all yes and of course we need also to know what what is that that's with flat what is
00:35:38
the key that we're looking for supper going want to search for key in that didn't national right
00:35:43
alright so oh well i said preconditions are the most important thing but actually
00:35:47
let me for the demonstration here let me write the post commission first
00:35:50
so you introduce suppose conditioned by the ensures keywords i hear i'm saying here comes the post condition
00:35:55
and the post condition is going to be more or less that if you look at
00:35:59
the at the re at that visit position you're going to see the key
00:36:04
so here i'm saying you to rely on after calling this routine that the admin and
00:36:10
that there are returned that's how parameters at that location you can find the key
00:36:15
well here we get it get some complaints already from from the verify or so
00:36:20
the verify as running in the background as some typing in this program
00:36:23
and it's complaining that the in the c. c. r. m. and may not be in the c. c. into data right
00:36:29
so i think that that nice strings and this by saying um that these are in
00:36:35
the um the indices into that the right and um it's alright um thanks
00:36:48
about that alright and i can see that that the number of fires happy
00:36:53
we're saying that okay this seems like an okay uh pose condition
00:36:57
but of course if we're gonna be able to ensure dispose condition there had better be such an element in the first place
00:37:02
so we introduce a precondition which we do with the requires keyword samples say that there exists a position i ga
00:37:09
in the re such that well essentially is that these um i'm a things all
00:37:18
and i i i this is for someone doing this example and from the crowd away so um these um
00:37:31
make tensions you can find my errors probably introduce some alright so that's the precondition well that's one of the preconditions
00:37:39
remember that we're also saying that this is only gonna work if we
00:37:42
have those monitor missy properties so we need some additional preconditions
00:37:46
that you can see that the preconditions i'm writing in this example they have on the fires uh like
00:37:51
this that that's probably not the first example that you would that you would show your um
00:37:55
you're young software engineers but i trust that that i can charities and that you're okay but that
00:38:02
so here i'm going to say well if we have uh some
00:38:06
cornet in the um uh in that direction and we have a
00:38:11
j. and ha prime in the other direction there to indices
00:38:17
and then uh it is the case that a. i. j.
00:38:24
is less or equal to a high j. prime okay
00:38:29
and we also are going to need it for the other directions let me write up on as well
00:38:33
so we haven't high and then i prime and um
00:38:37
if we see the seas or in this order
00:38:43
i owe much to to type but it all be worthwhile shirley alright okay i like that
00:38:57
that leaves something out this is going to allow us to write subtle bikes or snow
00:39:05
but we think that that
00:39:09
you know yes good uh_huh yes alright one week response in the back ah
00:39:20
alright so what are you not understanding about the specification should be um
00:39:25
so they're preconditions impose conditions preconditions are introduced by the keyword require suppose conditions by the keyword
00:39:31
ensures i'm trying to write down here what we want saddle back search to do
00:39:36
so writing down the spec is really important we need to get this right
00:39:41
we don't get the spec right mom we're not gonna get the program right that's going to do what we want
00:39:48
right so okay i did um i'm using in this specification
00:39:55
open fires which are more advanced and you um
00:39:58
they use mathematics and logic but the but i'm also writing a post condition which
00:40:03
is just a condition that you can write in in any language alright
00:40:08
okay let's let's plough ahead with guns with the um
00:40:12
writing some code and see where where we go okay so um
00:40:17
someone to write some some code and remember we're going to start here in
00:40:21
the in the upper left hand corner so i'm going to start m.
00:40:25
uh at zero and i'm going to start an ad well here we have this a decision to make
00:40:29
should we start and just one about the um just one about the or the the matrix
00:40:35
or should we always make sure that and and is an index into the matrix
00:40:40
well this is a a design decision that you also would make typically if you start from origin you would do it a
00:40:45
little bit differently but here i'm going to make sure that it's you did it all these years and i'm an index
00:40:51
so we're going to have a loop and and do is going to continue as long as the thing that we have is not the key
00:40:57
it's not clear that if this loop is ever going to terminate it would terminate when this condition doesn't hold
00:41:04
in other words it would terminate when we have found the key so if we can ever get there then this is going to do good thing
00:41:11
alright so um what sort of um invariance would be right for the loop
00:41:17
so a loop invariant is a condition that holds on every
00:41:20
iteration just before the loop guard is is evaluated
00:41:24
so we've said here already that m. we would like em to always be
00:41:29
uh in index into the right and would like and to always be an index into the right as well
00:41:36
okay so we're writing that down as a design decision that is worth thinking
00:41:40
these things never had that and then should always be in the seas
00:41:45
so if you writing this programming and you didn't think clearly about this you may very easily
00:41:49
step outside the bounds or do things in a program that's not gonna be quite right
00:41:55
okay so now we have another part of the invariant which
00:41:58
is remember those blue shaded regions in my my diagram
00:42:03
well they are essentially saying that we have a variation of of this
00:42:07
precondition so i'm i'm a copy that precondition down to to here
00:42:13
someone to say that there exist an element that is equal to the key that i
00:42:17
don't want to say that it exists somewhere in the in the whole ray
00:42:21
because we want to to be able to shrink that area to have a smaller area as we
00:42:25
go along with more loop iterations so um okay who can tell me how to change this
00:42:32
um hum this loop invariant to be what we want to be the blue shaded regions from from the diagrams
00:42:43
uh_huh uh_huh
00:42:50
oh
00:42:51
thank you very much so replace zero by am
00:42:56
so what we're saying here is that here we saying that
00:42:59
there exists an index somewhere between am and the um
00:43:04
and the and the the x. x. axis such that this holes great
00:43:09
okay and what we say about the um the other direction
00:43:18
um one subject oh
00:43:23
ah yes ah thank you so the suggestion is let's replace eight out um
00:43:28
uh the things by an and actually remember that we're we're going to um
00:43:35
yeah actually what we can see here this seems like a good suggesting 'cause that's going in that direction
00:43:39
here are getting in an error message that that complains about loop invariant violation
00:43:45
well but this is saying is that uh that this cannot be established initially and it is because
00:43:50
and usually usually we have we always use half open interval is but in this case is initialised and to be an
00:43:57
index so actually we want all jason are in uh that
00:44:03
or uh that can be as large as an itself
00:44:07
okay so this is not our goal we're gonna maintain this condition with every loop iteration
00:44:13
um alright well um how are we gonna do that to her writing the body of the loop now so and
00:44:21
now i'm getting a complaint that he can prove termination well of course i'm not doing
00:44:25
anything in them so we're not certainly this loop is not going to terminate
00:44:30
but it also reminds us of what what is the what is
00:44:34
what is going to make this terminate very often the tool would figure out that itself
00:44:38
but in this case it's little bit trickier so i'll i'll have to supply it
00:44:42
so here i'm going to supply a termination metric something that is going to decrease with every step through
00:44:48
and of course if you remember that diagram the diagram shrunk up the little white region
00:44:54
um each time so i can say here something that is going
00:44:58
to decrease always is what remains in the x. axis
00:45:02
plus what remains in the y. axis because why goes in the um uh goes
00:45:07
down in this case okay so now we're going to write the code
00:45:12
so how do we do that well we're certainly going to compare that current element with it um
00:45:19
with the with the key so it could be that it's less than the
00:45:23
key um or it could be that it's greater than the key
00:45:29
so if it is less than the key well then we would like to do
00:45:33
something that is going to eat increase the value of a and and
00:45:39
so we have two things to do we could either fiddle with am where we can fiddle with an
00:45:44
i remember an is going in the direction from zero upwards and and the scoring from the last
00:45:49
index downwards so which one of these to do we want to change in this case
00:45:59
uh_huh and ran
00:46:03
yeah okay alright so am goes upwards and uh well certainly and the other one must
00:46:09
be an right uh and there it is that is the correctness of the program
00:46:16
you know if you're writing this program and you didn't have this tool
00:46:20
uh let me guess what you might do you perhaps you didn't write down the specification to begin with
00:46:26
maybe you didn't explain carefully in the in the documentation that you needed these
00:46:30
two preconditions for saddle back search to to work in the first place
00:46:34
yeah so in particular you bought a precondition says that we're assuming that the element exists
00:46:40
we would have written a slightly different program if we didn't assume that the that the element existed in the first place
00:46:45
so that's one good thing but then once once we wrote down those loot
00:46:49
invariance it was and uh in this case the termination metric as well
00:46:53
it was clear what what operations that we had a available to us were we could increment m. or we could recommend and
00:47:01
now it's not always the case that that just putting those in like this would would
00:47:05
know all magically lead to the right program but in this case it does
00:47:08
but if you were true that you're doing it right now you're thinking in your head is
00:47:12
is really like it i think in some cases where this is not really right
00:47:16
well that that's the sort of thing that we do but if you know how to reason in
00:47:20
terms of invariance you reestablished invariant with every loop iteration and we prove that the loop terminates
00:47:26
and from the loop invariant uh and the mediation regards fall as opposed to this we want
00:47:31
so this program is now known to be correct and it's been proved to be correct
00:47:35
so my point here is that i think that the source of tools are the
00:47:39
ones that uh that young software engineers as they are learning to program
00:47:44
a can can make use of um and again this was more complicated than
00:47:48
the many of the introductory programs because i was using one fires
00:47:53
okay so um that made the move on will but that and but let me re emphasise the point again remember i said the
00:48:00
there are some routines that you're right that there's just no reason to making
00:48:05
a mistake but and the this i would say it's one of those
00:48:09
okay so let's see so in them the ten minutes i have left i'm going to say a few things about security um so
00:48:17
um i've talked about correctness so far would preconditions post conditions and invariance
00:48:22
and you also want to make sure that your programs are secure depending what sorts of programs or writing
00:48:27
and that this goes beyond the functional correctness in the following way that
00:48:32
if we're just writing a program ourselves we are our own any that is um
00:48:37
it's just we're trying to protect ourselves from making a mistake in the program
00:48:42
but when you deal with security you also have to me to to checks that no
00:48:46
add the series no attacker can somehow intercept what you what the program is doing
00:48:52
for example by looking at the messages that you're setting across the the network
00:48:56
and then try to do bad things with the program so
00:48:59
that goes beyond the the source of um a simple
00:49:04
a fungal correctness so i'm going to give you one little example um
00:49:08
and the these examples always have an allison a ball and so this does
00:49:13
too so the ideas alice is going to send the message to bob
00:49:17
and uh that's easy enough to do but now if someone reads what's going on on that on that
00:49:23
network you would immediately get am so we want to encode am in some sort of way
00:49:28
well we could write some function of them and send that across um that seems
00:49:34
good now we're not sending am so this uh perhaps has some some problems
00:49:39
and um but of course not all such functions are good ideas
00:49:43
for example if we just decide to um increment m. by one and thinking that that that's um
00:49:49
a a secret way of uh of getting the message to the other side we're probably mistaken
00:49:55
so what it comes down to is that with like
00:49:59
the whatever goes across the wire to look as if we're just sending something random
00:50:05
that is with like an uh an eavesdrop or to be able to
00:50:10
it should not be able to distinguish the actual execution from
00:50:14
uh from something that sense just a random number across that's uh essentially
00:50:19
it means um are part of it in a nutshell for you
00:50:22
um so uh in this case but we can't prove that these two programs are um are indistinguishable in eavesdrop
00:50:29
or would be able to distinguish these two programs but that's the that's that's the idea so um
00:50:35
we can we can do such security reasoning uh using program reasoning so if you know program
00:50:41
a program logic send you understand what the semantics of programs you can do this kind of reasoning
00:50:46
uh it's otherwise uh it's off and on for example in game based techniques or
00:50:50
what their number techniques i'm not going to go through them here but
00:50:54
if you want to do this would program reasoning that essentially what you're doing is you're
00:50:57
riding the specification and the specification is itself a program and it is one that
00:51:03
that you you would be happy with if that's what eavesdrop or looks at so for example
00:51:08
something that really sensor raw true random number across the wire you would be happy but
00:51:13
and then you implement uh your program and then you prove that you are indistinguishable
00:51:18
and there are various footnotes with indistinguishable you want to say that there
00:51:23
pull the normal time um indistinguishable that is that that if you give
00:51:28
the attacker only him resources computational resources that are a little mill
00:51:33
in the size of the problem that they would be able they will not be able to to figure out what's going on
00:51:39
i'll skip over those of footnotes so uh we build the
00:51:42
tool uh called quibble of that text equivalents that were
00:51:46
checks the in distinguish ability of programs and uh it has to back ends and both are basing formal methods
00:51:53
uh it uses the rose that back and and it uses rose
00:51:57
that as a as a down the model checkers actually
00:52:00
so that means that uh when uh when you feed a oh yeah i'm going to say
00:52:06
the inputs to quit like it's not just the program but it's two programs and it's a whole um
00:52:11
it's a proof that you think it's a proof for why uh why your program is correct
00:52:17
and we have like an checked that in two different ways can check it with words that were with actually
00:52:21
so what was at rose that is working like a bounded model checker which means that it's going to check this
00:52:27
uh this equivalence up to certain bounce then that means that it might find errors in that case was that
00:52:33
usually find some pretty quickly or it may not find any errors and done well maybe it is correct
00:52:39
and uh once you uh you get enough made easy uh you're you have enough
00:52:44
confidence that you might want to spend the effort trying to really prove it
00:52:47
so then you can use daphne in this case daphne is really use
00:52:50
just as a logical foundation as a proof um as a um
00:52:54
prevention for it and it can then with your help uh it gets too yes answer if you're
00:53:00
protocol really is correct so things look a little bit like this in the in the quit long notation
00:53:05
that you have the um the ideal program in this case the left uh where
00:53:09
you can see that what is being sent this just a a random number
00:53:13
and then on the on the right i'm using the uh the well
00:53:17
in this case faulty program that's going to send em plus one
00:53:21
and you can see in the query language that you can set up an adversary as and the adversaries are uh
00:53:28
uh you um you tell the pro you you make it part of
00:53:32
your program where an adversary can them um can be part of
00:53:36
um of things in this case we're saying that in the network itself
00:53:39
is the adversary so um anything can happen at some point
00:53:44
uh alright so the way that you prove indistinguishable lydia programs in gridlock is that
00:53:48
you start with the ideal program and you do program transformations on it
00:53:53
and it's these program transformations art that are checked so this is
00:53:57
a this is not an um as automatic process as
00:54:01
it was to to write settle back surgeon in that i think you have to work a lot more here um
00:54:07
and the i'm giving you some examples on the slide as to what these
00:54:10
transformations are for example you might re factor these objects in some ways
00:54:14
you might have some assumptions lying around that you can appeal to
00:54:17
and you might um establish some some data invariance which are
00:54:21
really just like the variance are talked about and you might make use of those somewhere in the in these proves developments
00:54:27
so that is essentially what what a quick like those so you can use
00:54:33
formal methods uh not only for functional correctness but also going
00:54:36
beyond that for for security and that's really important
00:54:40
so let me conclude so at the heart of formal methods are specifications
00:54:44
we write specifications for what we want one things to do
00:54:48
um some people stop it just riding specifications in the model them in some way where they
00:54:53
check to specifications for error and then they think of the code writing process as
00:54:57
being a separate process that's still making you some some formal methods but you might also
00:55:02
try to connect it to get the code to be formally verified mechanically verified
00:55:07
to um to live up to the specifications as we saw in the in the daffy them all
00:55:12
but in any case it helps you with that reasoning because when you write down
00:55:16
the the loop invariance when you write down the various preconditions you're thinking
00:55:20
in terms of what is it they're really need here what should all that which points in the program and that makes you better software engineer
00:55:27
so um my advice to the the young software engineers is
00:55:32
trial quantities um programmer fires uh for example daffy has a
00:55:36
tutorial you can try online or a install it
00:55:38
on your own machine is much more fun 'cause then it's uh it runs um as your um
00:55:43
at your typing in the program which really changes your mind as to i mean what what these things really can do for you what you can
00:55:50
you get disappointed when your c. p. u. doesn't does not do this for you and in other i. d.s afterwards
00:55:56
then if your teacher i would suggest uh might vices incorporate these sorts of things that is when
00:56:02
you think about algorithms when you think about programming and data structures uh loops think about invariance
00:56:09
that point output the preconditions are we need preconditions we need to think in terms of
00:56:13
these things to to get our programs to work and um that having that
00:56:18
uh that common framework for it uh and setting that early i think would be a really great thing
00:56:24
so um for the future software engineering i think that we have a have a great
00:56:28
future and uh so i'd like to thank you for attention and program safely
00:56:41
i think you know it
00:56:49
her daughter will have time for some questions uh
00:56:58
but the high tech for a ride a bus are towards up here
00:57:06
mike's or order yeah whatever once i guess
00:57:14
the extra stuff for a for a wonderful talk i teach software engineering undergrad software
00:57:19
engineering and actually actually start using daphne no perfect them so this last right
00:57:25
um so i have two questions uh one is that you are good at an interactive for
00:57:31
him was to wonder just yes no uh is more useful because of shape thinking
00:57:38
for south exit or nice but what about other kind of cold like stuff that's more t.
00:57:45
v. connected to each of our like you're writing a a file system are out
00:57:50
you know where you end up having to really spend a lot of time on week
00:57:54
let's think about a lot of the calls conditions so things become very complex and does it
00:58:00
become distracting especially when you have or some fireworks like it uses a particular you
00:58:06
know first order logic inside why did you kind of forget what you're gonna write interface
00:58:13
e. you can get lost in the in using the tool and the tools
00:58:17
uh even though they they're really very good these days they they still have a
00:58:20
lot of wrinkles so um um but the the um i think that one
00:58:27
one difference between the those are the pushbutton and the then the interactive then i should say i should make it clear that
00:58:33
if we could get more things to be automatic uh of course i'm all for for that
00:58:37
i mean there's no reason to to add more work onto the already overloaded software engineer
00:58:43
but i i just uh want to argue that the interactivity that is there when it is
00:58:47
needed is not is not an overall that thing so when you write something like um
00:58:53
if you're trying to write specifications for something that someone else already wrote
00:58:58
then trying to in for them and having as much automation as possible is
00:59:02
is a really good thing 'cause then there is some very tricky to
00:59:05
figure out with these things are afterwards but if it's cool that you're right then i think that interactivity is is a really nice thing
00:59:12
and if you have something like a file system that these things do get
00:59:15
complicated and then that's one formal methods can help me even more
00:59:19
because you you abstract and you try to simplify and you write down uh the things that that matter
00:59:25
um but but yes or wrinkles in the tools to thank you and if i may ask a follow up question huh
00:59:32
so that they're what to show that's is in some sense stacked even below right the spec yep right the coding
00:59:38
mind of task depending on where you write the test and then the call this size but the tests yeah
00:59:43
um and that is my understanding that the really take off a
00:59:47
while impact is because software engineers under time pressure and
00:59:52
like what s. dive right into writing the code uh_huh and you know if they have to spend
00:59:57
right the time reading task before handing the like yeah so that's that's kind of the human angle
01:00:04
this is something you already know how has that shaped you're thinking about
01:00:09
proposing spectral and development and are there ways to mitigate that every human desire to
01:00:15
your deadline is yeah um when i was a young software a software engineer
01:00:21
a i a lot about these techniques i thought they were really great and i
01:00:25
thought all wonderful now i can do all my development as this way
01:00:29
that i think is a mistake yeah that is um but it's it's
01:00:34
going to take us a long time before all software engineering is
01:00:36
is that is done this way if for no other reason that
01:00:39
that correctness they're correct this is a spectrum um and um
01:00:45
i think that the way to to approach that is that um that
01:00:49
there's certain routines that you learn are that you want you
01:00:53
know these sorts of techniques they're certain routines that you think in your had this one i just don't wanna make any mistakes
01:01:00
and then you apply these techniques and the other cases where uh let's say that you write lot of java coder lots
01:01:05
of 'em delegates being passed around here and there uh i don't know how to write to specs um they're
01:01:12
testing is probably more effective there uh to uh to figure things out so finding those engineering trade offs is something
01:01:19
that that um i mean that we all need to learn as a community but also as a software dinners
01:01:25
thank you thank you or style and here
01:01:31
right that'd huh thank you yes or it was a worry in his buying the
01:01:37
example that you gave me one thing i i thought about when you say that the the
01:01:43
you you could environmental does god terminates all the calls conditions on the whole uh_huh
01:01:47
i was thinking impact is uh it's not you know that the whole will terminate eventually
01:01:53
yeah you did you to terminate it in that in some reasonable time so
01:01:57
ah what about the like a simple to complex in general in
01:02:01
about the fourth performance reasoning uh in the state of the art it
01:02:05
and you do some things like like you did on the screen
01:02:08
for performance that's right yeah thank you for that price in the so
01:02:14
even when you um it for daphne in particular daphne checks that that your
01:02:20
program is correct and that it will eventually terminate it will not check
01:02:25
uh at that the uh the time in which it terminates is something that
01:02:29
you have to spend a that is you don't you may not
01:02:32
the light this on may not be shining anymore when that when your program terminates uh it also
01:02:37
does not check that you have the space requirements needed those are the things that it
01:02:40
doesn't jack so with with daphne if you try to do something like that what you would
01:02:44
do is you would set up something that you that would let let you count
01:02:48
the number of loop iterations which in this case you can because them the decreases gloss was a it was an image or
01:02:55
so you can just compute that what it is a up front which is the the some of the two dimensions
01:03:01
and uh so in that case you can you can find of performance down but in
01:03:05
many other cases you may um that maybe much trickier to uh to compute
01:03:11
so in principle you could do it with a bike instrument thing a a daffy
01:03:16
program but there are also other tools that that would do it for you
01:03:19
and those things are certain important that also for like real time programs that thank you yep x.
01:03:29
i also the question yes thanks a lot for the interesting talk um i have a question about the uh really sure of
01:03:36
um basically the lines of code in quotes uh between specifications and uh
01:03:41
actual a code that you are specifying the specifications because you mentioned
01:03:47
uh one example where you have ten thousand lines of code uh and that is
01:03:51
basically specified by five hundred yeah i wasn't i think so yeah uh yeah
01:03:56
lines of specs yeah staggering numbers yeah and and
01:04:00
you doesn't example was also and not that's that's started difference but uh
01:04:05
also you had a lot more characters specifying than coding now um
01:04:11
at some point don't you get a a problem that you have too much of box
01:04:17
much more bucks in your spec then your program yep so in the what when you do the development
01:04:23
it very often happens that uh let's say for you leave something out of the the the specification
01:04:30
but you realise that then at some point during the development work when you're trying to to reason about the loop
01:04:35
that you either forget some conjoined or that you write them incorrectly for example it was very easy to have written
01:04:41
yeah for the j. if you remember that to say let's strictly less than a ducklings
01:04:45
one that rather than less or equal to which is what this example needs
01:04:49
so many of those things happen and you correct as many things in the specs as you would in in the programs
01:04:54
um that s. for the ratio i i think that the uh daphne has has seen a
01:05:00
lot better ratios then uh then uh many other tools um there been some some measurements
01:05:08
especially in the uh in the ironclad unearthly projects that use a daffy
01:05:12
for for system a system code uh that was the um
01:05:17
um so there the well the the overhead there was about five soaps for
01:05:23
between four and six lines of overhead for every line of executable code
01:05:28
so i mean that's that seems a lot better but but even as i said you know
01:05:31
with this staggering five hundred thousand lines for ten thousand executable i mean it just seems
01:05:37
seems i'm so out of proportion but even with those numbers uh that were measured as i said that the
01:05:43
the additional cost was just two or three times which means that that in
01:05:47
the best track this is you spend a lot of time trying to
01:05:50
debug things and um and figure out what the errors are and and
01:05:53
things like that um but yeah that's specs can be unwieldy to
01:05:59
so so the basically based on the on those findings box in the spec are easier to find
01:06:04
and the bugs in the code no i'm an hour they i are easier i'm not sure uh
01:06:10
um i have written pieces of code that where the code has happened to be correct
01:06:16
but the this there's a some error in this back and i'm tearing my hair
01:06:20
out trying to figure out what's going wrong and then i realise all
01:06:23
well i forgot to say something so i'm not sure if it's easier in the in the program or not i'm not you you could also try
01:06:30
checking these at run time which is a which is a fine idea that when you get to more complicated data structures
01:06:37
um with um let's say a recursive data structures or something that uses these qualifiers then
01:06:42
you might take quite a bit of a performance it to to do it but
01:06:46
if you if you just check for for parameter validation things at run time that's a
01:06:50
that's a really good idea to uh for checking these things and it's cheap
01:06:55
uh unfortunately we're a little bit uh behind the schedule as often happens with software engineering informal methods that
01:07:02
well i think in the interest of time or like to think i our first speaker today

Share this talk: 


Conference program

Welcome address
Andreas Mortensen, Vice President for Research, EPFL
7 June 2018 · 9:49 a.m.
Introduction
Jim Larus, Dean of IC School, EPFL
7 June 2018 · 10 a.m.
The Young Software Engineer’s Guide to Using Formal Methods
K. Rustan M. Leino, Amazon
7 June 2018 · 10:16 a.m.
Safely Disrupting Computer Networks with Software
Katerina Argyraki, EPFL
7 June 2018 · 11:25 a.m.
Short IC Research Presentation 2: Gamified Rehabilitation with Tangible Robots
Arzu Guneysu Ozgur, EPFL (CHILI)
7 June 2018 · 12:15 p.m.
Short IC Research Presentation 3: kickoff.ai
Lucas Maystre, Victor Kristof, EPFL (LCA)
7 June 2018 · 12:19 p.m.
Short IC Research Presentation 5: CleanM
Stella Giannakopoulo, EPFL (DIAS)
7 June 2018 · 12:25 p.m.
Short IC Research Presentation 6: Understanding Cities through Data
Eleni Tzirita Zacharatou, EPFL (DIAS)
7 June 2018 · 12:27 p.m.
Short IC Research Presentation 7: Datagrowth and application trends
Matthias Olma, EPFL (DIAS)
7 June 2018 · 12:31 p.m.
Short IC Research Presentation 8: Point Cloud, a new source of knowledge
Mirjana Pavlovic, EPFL (DIAS)
7 June 2018 · 12:34 p.m.
Short IC Research Presentation 9: To Click or not to Click?
Eleni Tzirita Zacharatou, EPFL (DIAS)
7 June 2018 · 12:37 p.m.
Short IC Research Presentation 10: RaaSS Reliability as a Software Service
Maaz Mohiuddlin, LCA2, IC-EPFL
7 June 2018 · 12:40 p.m.
Short IC Research Presentation 11: Adversarial Machine Learning in Byzantium
El Mahdi El Mhamdi, EPFL (LPD)
7 June 2018 · 12:43 p.m.
20s pitch 1: Cost and Energy Efficient Data Management
Utku Sirin, (DIAS)
7 June 2018 · 2:20 p.m.
20s pitch 2: Gamification of Rehabilitation
Arzu Guneysu Ozgur, EPFL (CHILI)
7 June 2018 · 2:21 p.m.
20s pitch 4: Neural Network Guided Expression Transformation
Romain Edelmann, EPFL (LARA)
7 June 2018 · 2:21 p.m.
20s pitch 5: Unified, High Performance Data Cleaning
Stella Giannakopoulo, EPFL (DIAS)
7 June 2018 · 2:21 p.m.
20s pitch 6: Interactive Exploration of Urban Data with GPUs
Eleni Tzirita Zacharatou, EPFL (DIAS)
7 June 2018 · 2:22 p.m.
20s pitch 7: Interactive Data Exploration
Matthias Olma, EPFL (DIAS)
7 June 2018 · 2:22 p.m.
20s pitch 8: Efficient Point Cloud Processing
Mirjana Pavlovic, EPFL (DIAS)
7 June 2018 · 2:23 p.m.
20s pitch 9: To Click or not to Click?
Eleni Tzirita Zacharatou, EPFL (DIAS)
7 June 2018 · 2:24 p.m.
20s pitch 10: RaaSS Reliability as a Software Service
Maaz Mohiuddlin, LCA2, IC-EPFL
7 June 2018 · 2:24 p.m.
20s pitch 11: Adversarial Machine Learning in Byzantium
El Mahdi El Mhamdi, EPFL (LPD)
7 June 2018 · 2:24 p.m.
Machine Learning: Alchemy for the Modern Computer Scientist
Erik Meijer, Facebook
7 June 2018 · 2:29 p.m.

Recommended talks

Discoverying Life patterns
Fausto Giunchiglia, from University of Trento, Italy
8 June 2015 · 4:07 p.m.