WEBVTT

1
00:00:05.535 --> 00:00:06.655
<00:00:05.535>I <00:00:05.871>was <00:00:06.207>already <00:00:06.543>introduced.

2
00:00:06.835 --> 00:00:07.895
<00:00:06.835>My <00:00:07.073>name <00:00:07.311>is <00:00:07.550>on <00:00:07.789>Kasim.

3
00:00:08.395 --> 00:00:11.455
<00:00:08.395>I'm <00:00:08.535>working <00:00:08.674>as <00:00:08.815>a <00:00:08.955>cloud <00:00:09.094>engineer <00:00:09.235>at <00:00:09.375>Sidio <00:00:09.514>as <00:00:09.655>a <00:00:09.795>co-founder

4
00:00:12.165 --> 00:00:16.205
<00:00:12.165>also, <00:00:12.364>and <00:00:12.565>we <00:00:12.764>are <00:00:12.965>placed <00:00:13.165>in <00:00:13.364>vi <00:00:13.565>Vietnam.

5
00:00:16.425 --> 00:00:19.025
<00:00:16.425>So <00:00:16.600>if <00:00:16.775>you <00:00:16.950>want <00:00:17.125>there, <00:00:17.300>you <00:00:17.475>can <00:00:17.650>visit <00:00:17.825>us.

6
00:00:22.185 --> 00:00:26.585
<00:00:22.185>So <00:00:22.465>the <00:00:22.744>agenda <00:00:23.025>today, <00:00:23.305>before <00:00:23.584>I

7
00:00:27.355 --> 00:00:30.505
<00:00:27.355>start, <00:00:27.495>I <00:00:27.635>want <00:00:27.775>to <00:00:27.915>take <00:00:28.055>about, <00:00:28.195>uh, <00:00:28.335>talk <00:00:28.475>about <00:00:28.615>the <00:00:28.755>goals

8
00:00:30.925 --> 00:00:32.425
<00:00:30.925>and <00:00:31.195>the <00:00:31.465>motivation <00:00:31.735>of <00:00:32.004>the <00:00:32.275>talk.

9
00:00:34.475 --> 00:00:39.335
<00:00:34.475>And <00:00:34.650>afterwards <00:00:34.825>I <00:00:35.000>will <00:00:35.175>have <00:00:35.350>a <00:00:35.525>short, <00:00:35.700>uh, <00:00:35.875>introduction

10
00:00:39.675 --> 00:00:44.135
<00:00:39.675>or <00:00:39.815>a <00:00:39.955>short, <00:00:40.095>uh, <00:00:40.235>part <00:00:40.375>where <00:00:40.515>I <00:00:40.654>talk <00:00:40.794>about <00:00:40.934>social <00:00:41.074>testing

11
00:00:44.395 --> 00:00:46.615
<00:00:44.395>and <00:00:44.628>what's <00:00:44.861>the <00:00:45.095>difference <00:00:45.328>to <00:00:45.561>software <00:00:45.795>verification.

12
00:00:48.345 --> 00:00:51.405
<00:00:48.345>And <00:00:48.519>afterwards <00:00:48.695>I <00:00:48.870>will <00:00:49.045>talk <00:00:49.220>about <00:00:49.394>the, <00:00:49.570>our <00:00:49.745>logic.

13
00:00:53.085 --> 00:00:56.665
<00:00:53.085>And <00:00:53.212>I <00:00:53.339>will <00:00:53.466>not <00:00:53.594>tease <00:00:53.721>you <00:00:53.848>guys <00:00:53.975>a <00:00:54.103>lot <00:00:54.230>with <00:00:54.357>it <00:00:54.485>just

14
00:00:56.665 --> 00:00:59.105
<00:00:56.665>to <00:00:56.865>have <00:00:57.065>a <00:00:57.265>basic <00:00:57.464>understanding <00:00:57.665>what <00:00:57.865>it <00:00:58.065>is

15
00:01:01.035 --> 00:01:03.335
<00:01:01.035>and <00:01:01.268>followed <00:01:01.501>by <00:01:01.735>state <00:01:01.968>of <00:01:02.201>the <00:01:02.434>art,

16
00:01:03.475 --> 00:01:07.415
<00:01:03.475>how <00:01:03.615>software <00:01:03.755>validation <00:01:03.895>is <00:01:04.035>used <00:01:04.175>today <00:01:04.315>and <00:01:04.455>if <00:01:04.595>it's <00:01:04.735>even <00:01:04.875>used.

17
00:01:09.455 --> 00:01:13.035
<00:01:09.455>And <00:01:09.562>in <00:01:09.670>the <00:01:09.778>end <00:01:09.885>I <00:01:09.993>will <00:01:10.101>show <00:01:10.208>you <00:01:10.316>an <00:01:10.424>example <00:01:10.531>with <00:01:10.639>open <00:01:10.747>Jamie <00:01:10.855>l

18
00:01:15.025 --> 00:01:17.085
<00:01:15.025>and <00:01:15.305>how <00:01:15.585>this <00:01:15.865>can <00:01:16.145>be <00:01:16.425>done.

19
00:01:17.315 --> 00:01:21.405
<00:01:17.315>Also, <00:01:17.548>um, <00:01:17.781>with <00:01:18.015>the <00:01:18.248>help <00:01:18.481>of <00:01:18.715>AI

20
00:01:21.545 --> 00:01:22.645
<00:01:21.545>or <00:01:21.743>not, <00:01:21.941>we <00:01:22.139>will <00:01:22.337>see <00:01:22.535>it.

21
00:01:23.545 --> 00:01:27.315
<00:01:23.545>So <00:01:23.700>first <00:01:23.856>of <00:01:24.011>all, <00:01:24.167>the <00:01:24.322>goal <00:01:24.478>of <00:01:24.633>this <00:01:24.789>talk <00:01:24.945>is

22
00:01:29.395 --> 00:01:31.715
<00:01:29.395>I <00:01:29.628>really <00:01:29.861>want <00:01:30.095>to <00:01:30.328>raise <00:01:30.561>awareness <00:01:30.795>for

23
00:01:32.355 --> 00:01:34.435
<00:01:32.354>software <00:01:32.704>verification <00:01:33.054>since <00:01:33.404>a <00:01:33.755>lot

24
00:01:34.435 --> 00:01:35.755
<00:01:34.435>of <00:01:34.672>people <00:01:34.910>are <00:01:35.147>doing <00:01:35.385>software <00:01:35.622>testing,

25
00:01:35.815 --> 00:01:38.955
<00:01:35.815>but <00:01:35.990>verification <00:01:36.164>is <00:01:36.340>something <00:01:36.515>we <00:01:36.690>learn <00:01:36.865>in <00:01:37.039>the <00:01:37.215>university

26
00:01:38.975 --> 00:01:40.595
<00:01:38.975>and <00:01:39.208>then <00:01:39.441>we <00:01:39.675>never <00:01:39.908>do <00:01:40.141>it <00:01:40.375>again.

27
00:01:41.255 --> 00:01:43.395
<00:01:41.255>It <00:01:41.488>was <00:01:41.721>at <00:01:41.955>least <00:01:42.188>in <00:01:42.421>my <00:01:42.655>case.

28
00:01:47.245 --> 00:01:49.185
<00:01:47.245>So, <00:01:47.420>and <00:01:47.595>also <00:01:47.770>I <00:01:47.945>want <00:01:48.120>to <00:01:48.295>inspire <00:01:48.470>you <00:01:48.645>guys

29
00:01:49.525 --> 00:01:51.705
<00:01:49.525>to <00:01:49.805>think <00:01:50.085>further <00:01:50.365>about <00:01:50.645>this <00:01:50.925>topic

30
00:01:51.765 --> 00:01:54.585
<00:01:51.765>and <00:01:51.920>opportunities <00:01:52.076>in <00:01:52.231>this <00:01:52.387>area, <00:01:52.542>what <00:01:52.698>we <00:01:52.853>can <00:01:53.009>do <00:01:53.165>maybe

31
00:01:54.585 --> 00:01:55.865
<00:01:54.585>with <00:01:55.161>AI <00:01:55.737>better

32
00:01:56.285 --> 00:01:57.825
<00:01:56.285>and <00:01:56.515>what <00:01:56.747>we <00:01:56.978>can <00:01:57.209>do <00:01:57.440>with <00:01:57.671>AI

33
00:01:58.565 --> 00:02:01.385
<00:01:58.565>to <00:01:58.740>maybe <00:01:58.914>replace <00:01:59.090>even <00:01:59.265>software <00:01:59.440>testing <00:01:59.615>here <00:01:59.789>and <00:01:59.965>there.

34
00:02:04.605 --> 00:02:05.825
<00:02:04.605>So <00:02:04.971>the <00:02:05.337>motivation <00:02:05.703>itself,

35
00:02:06.405 --> 00:02:08.905
<00:02:06.405>AI <00:02:06.605>generates <00:02:06.805>software <00:02:07.005>actually <00:02:07.205>was <00:02:07.405>the <00:02:07.605>main <00:02:07.805>motivation

36
00:02:08.905 --> 00:02:10.545
<00:02:08.905>where <00:02:09.138>I <00:02:09.371>get <00:02:09.604>to <00:02:09.838>know <00:02:10.071>that <00:02:10.305>more

37
00:02:10.545 --> 00:02:13.505
<00:02:10.544>and <00:02:10.700>more <00:02:10.856>people <00:02:11.011>are <00:02:11.167>working <00:02:11.322>with <00:02:11.478>AI <00:02:11.633>generated <00:02:11.789>code <00:02:11.945>instead

38
00:02:13.505 --> 00:02:14.745
<00:02:13.505>of <00:02:13.691>writing <00:02:13.877>the <00:02:14.063>code <00:02:14.249>on <00:02:14.435>its <00:02:14.621>own.

39
00:02:15.525 --> 00:02:19.745
<00:02:15.525>And <00:02:15.665>I <00:02:15.805>know <00:02:15.945>that <00:02:16.085>testing <00:02:16.225>my <00:02:16.365>own <00:02:16.505>code <00:02:16.645>is <00:02:16.785>really <00:02:16.925>sometimes

40
00:02:19.855 --> 00:02:22.905
<00:02:19.855>hard, <00:02:20.030>but <00:02:20.204>if <00:02:20.380>you <00:02:20.554>have <00:02:20.730>to <00:02:20.905>test <00:02:21.079>your <00:02:21.255>test,

41
00:02:22.905 --> 00:02:24.225
<00:02:22.905>the <00:02:23.301>AI <00:02:23.697>generated <00:02:24.093>code,

42
00:02:24.565 --> 00:02:26.185
<00:02:24.565>it <00:02:24.740>might <00:02:24.915>be <00:02:25.090>the <00:02:25.265>case <00:02:25.440>that <00:02:25.615>you <00:02:25.790>really <00:02:25.965>lost.

43
00:02:26.285 --> 00:02:28.305
<00:02:26.285>And <00:02:26.440>even <00:02:26.596>there <00:02:26.751>you <00:02:26.907>have <00:02:27.062>to <00:02:27.218>be <00:02:27.373>much <00:02:27.529>more <00:02:27.685>careful.

44
00:02:28.325 --> 00:02:29.865
<00:02:28.325>You <00:02:28.555>have <00:02:28.787>to <00:02:29.018>write <00:02:29.249>much <00:02:29.480>more <00:02:29.711>tests

45
00:02:30.395 --> 00:02:33.385
<00:02:30.395>since <00:02:30.550>you <00:02:30.706>really <00:02:30.861>don't <00:02:31.017>know <00:02:31.172>what <00:02:31.328>the <00:02:31.483>code <00:02:31.639>is <00:02:31.795>doing,

46
00:02:33.405 --> 00:02:35.145
<00:02:33.405>if <00:02:33.638>you <00:02:33.871>don't <00:02:34.105>analyze <00:02:34.338>it <00:02:34.571>in <00:02:34.805>detail.

47
00:02:35.525 --> 00:02:38.305
<00:02:35.525>But <00:02:35.725>if <00:02:35.925>you <00:02:36.125>analyze <00:02:36.325>it <00:02:36.525>in <00:02:36.725>detail, <00:02:36.925>then

48
00:02:38.965 --> 00:02:41.585
<00:02:38.965>at <00:02:39.165>some <00:02:39.365>point <00:02:39.565>the <00:02:39.765>question <00:02:39.965>will <00:02:40.165>prompt, <00:02:40.365>uh,

49
00:02:41.805 --> 00:02:44.745
<00:02:41.805>to <00:02:41.921>just <00:02:42.038>ask <00:02:42.155>yourself <00:02:42.271>why <00:02:42.388>you <00:02:42.505>don't <00:02:42.621>write <00:02:42.738>it <00:02:42.855>on <00:02:42.971>your <00:02:43.088>own <00:02:43.205>if

50
00:02:45.085 --> 00:02:47.425
<00:02:45.085>you <00:02:45.318>analyze <00:02:45.551>it, <00:02:45.785>the <00:02:46.018>whole <00:02:46.251>code <00:02:46.485>again.

51
00:02:48.785 --> 00:02:51.565
<00:02:48.785>But <00:02:49.065>again, <00:02:49.345>AI <00:02:49.625>is <00:02:49.905>something <00:02:50.185>probabilistic

52
00:02:52.745 --> 00:02:56.325
<00:02:52.745>and <00:02:52.885>this <00:02:53.025>means <00:02:53.165>that <00:02:53.305>it <00:02:53.445>might <00:02:53.585>generate <00:02:53.725>errors, <00:02:53.865>maybe <00:02:54.005>not <00:02:54.145>here

53
00:02:56.325 --> 00:02:58.885
<00:02:56.325>and <00:02:56.480>there, <00:02:56.636>but <00:02:56.791>at <00:02:56.947>some <00:02:57.102>point <00:02:57.258>it <00:02:57.413>might <00:02:57.569>generate <00:02:57.725>errors.

54
00:02:59.655 --> 00:03:03.525
<00:02:59.655>And <00:02:59.782>for <00:02:59.909>this, <00:03:00.036>the <00:03:00.164>code <00:03:00.291>has <00:03:00.418>to <00:03:00.545>be <00:03:00.673>validated <00:03:00.800>in <00:03:00.927>this <00:03:01.055>sense

55
00:03:03.545 --> 00:03:05.285
<00:03:03.545>and <00:03:03.825>test <00:03:04.105>might <00:03:04.385>not <00:03:04.665>be <00:03:04.945>enough.

56
00:03:07.165 --> 00:03:09.025
<00:03:07.165>And <00:03:07.398>it's, <00:03:07.631>and <00:03:07.864>it's <00:03:08.098>also <00:03:08.331>not <00:03:08.565>easy

57
00:03:09.025 --> 00:03:10.905
<00:03:09.025>to <00:03:09.180>write <00:03:09.336>tests <00:03:09.491>if <00:03:09.647>you <00:03:09.802>have <00:03:09.958>a <00:03:10.113>black <00:03:10.269>box <00:03:10.425>actually

58
00:03:10.905 --> 00:03:12.785
<00:03:10.905>where <00:03:11.080>you <00:03:11.255>don't <00:03:11.430>know <00:03:11.605>how <00:03:11.780>the <00:03:11.955>inputs <00:03:12.130>look <00:03:12.305>like

59
00:03:12.805 --> 00:03:14.425
<00:03:12.805>and <00:03:13.085>how <00:03:13.365>the <00:03:13.645>output <00:03:13.925>should <00:03:14.205>be.

60
00:03:17.955 --> 00:03:19.815
<00:03:17.954>So, <00:03:18.234>and <00:03:18.515>what <00:03:18.795>is <00:03:19.075>software <00:03:19.355>testing

61
00:03:19.875 --> 00:03:21.335
<00:03:19.875>and <00:03:20.203>what <00:03:20.532>is <00:03:20.860>software <00:03:21.189>validation?

62
00:03:26.245 --> 00:03:28.385
<00:03:26.245>So <00:03:26.445>just <00:03:26.645>software <00:03:26.845>testing, <00:03:27.045>I <00:03:27.245>guess <00:03:27.445>everyone <00:03:27.645>knows

63
00:03:28.385 --> 00:03:29.425
<00:03:28.385>what <00:03:28.697>software <00:03:29.009>testing <00:03:29.321>is.

64
00:03:29.535 --> 00:03:31.505
<00:03:29.535>It's <00:03:29.734>the <00:03:29.935>execution <00:03:30.135>of <00:03:30.335>some <00:03:30.535>piece <00:03:30.734>of <00:03:30.935>code.

65
00:03:31.775 --> 00:03:34.025
<00:03:31.775>With <00:03:32.125>selected <00:03:32.475>inputs, <00:03:32.825>you <00:03:33.175>have

66
00:03:35.875 --> 00:03:39.215
<00:03:35.875>to <00:03:36.075>use <00:03:36.275>a <00:03:36.475>huge <00:03:36.675>amount <00:03:36.875>of <00:03:37.075>input <00:03:37.275>data

67
00:03:39.275 --> 00:03:42.335
<00:03:39.275>to <00:03:39.475>have <00:03:39.675>valid <00:03:39.875>test <00:03:40.075>actually <00:03:40.275>and <00:03:40.475>completely <00:03:40.675>valid.

68
00:03:42.555 --> 00:03:43.815
<00:03:42.555>You <00:03:42.838>can't <00:03:43.122>really <00:03:43.405>get <00:03:43.689>there.

69
00:03:45.435 --> 00:03:48.585
<00:03:45.435>Yeah, <00:03:45.635>except <00:03:45.835>you <00:03:46.035>have <00:03:46.235>a <00:03:46.435>function <00:03:46.635>like, <00:03:46.835>uh,

70
00:03:49.125 --> 00:03:53.745
<00:03:49.125>add <00:03:49.265>1, <00:03:49.405>2, <00:03:49.545>2 <00:03:49.685>and <00:03:49.825>uh, <00:03:49.965>whole <00:03:50.105>function <00:03:50.245>does <00:03:50.385>nothing <00:03:50.525>else.

71
00:03:53.745 --> 00:03:56.345
<00:03:53.745>Then <00:03:53.885>adding <00:03:54.025>one <00:03:54.165>number <00:03:54.305>to <00:03:54.445>the <00:03:54.585>other <00:03:54.725>one, <00:03:54.865>then <00:03:55.005>it's <00:03:55.145>valid

72
00:03:56.365 --> 00:03:59.585
<00:03:56.365>of <00:03:56.520>course, <00:03:56.676>but <00:03:56.831>you <00:03:56.987>normally <00:03:57.142>don't <00:03:57.298>have <00:03:57.453>functions <00:03:57.609>like <00:03:57.765>that.

73
00:04:01.155 --> 00:04:03.495
<00:04:01.155>But, <00:04:01.355>but <00:04:01.555>the <00:04:01.755>software <00:04:01.955>verification <00:04:02.155>in <00:04:02.355>this <00:04:02.555>sense,

74
00:04:03.975 --> 00:04:07.575
<00:04:03.975>software <00:04:04.150>verification <00:04:04.325>is <00:04:04.500>a <00:04:04.674>formal <00:04:04.850>proof <00:04:05.025>of <00:04:05.200>a <00:04:05.375>program

75
00:04:08.645 --> 00:04:10.655
<00:04:08.645>that <00:04:08.925>it <00:04:09.205>confirms <00:04:09.485>to <00:04:09.765>the <00:04:10.045>specification.

76
00:04:10.915 --> 00:04:14.055
<00:04:10.915>And <00:04:11.114>this <00:04:11.315>also <00:04:11.515>means <00:04:11.715>that <00:04:11.915>the <00:04:12.114>whole <00:04:12.315>logic,

77
00:04:14.155 --> 00:04:16.055
<00:04:14.155>the <00:04:14.388>operational <00:04:14.621>logic <00:04:14.855>has <00:04:15.088>to <00:04:15.321>be <00:04:15.555>correct

78
00:04:16.595 --> 00:04:18.095
<00:04:16.595>for <00:04:17.045>all <00:04:17.495>admissible <00:04:17.945>inputs.

79
00:04:20.255 --> 00:04:24.715
<00:04:20.255>And <00:04:20.394>if <00:04:20.534>you <00:04:20.675>compare <00:04:20.815>this <00:04:20.954>to, <00:04:21.094>if, <00:04:21.235>if <00:04:21.375>you <00:04:21.515>compare <00:04:21.654>this

80
00:04:24.715 --> 00:04:25.875
<00:04:24.715>to <00:04:25.236>software <00:04:25.759>verification

81
00:04:25.875 --> 00:04:27.395
<00:04:25.875>and <00:04:26.148>software <00:04:26.422>testing, <00:04:26.695>then <00:04:26.969>we <00:04:27.243>see

82
00:04:28.225 --> 00:04:29.955
<00:04:28.225>that <00:04:28.505>the <00:04:28.785>whole <00:04:29.065>things <00:04:29.345>are <00:04:29.625>different.

83
00:04:29.955 --> 00:04:31.155
<00:04:29.955>Like <00:04:30.224>the <00:04:30.495>goal <00:04:30.765>is <00:04:31.034>different.

84
00:04:31.155 --> 00:04:33.715
<00:04:31.155>Like <00:04:31.282>on <00:04:31.409>the <00:04:31.536>one <00:04:31.664>hand <00:04:31.791>we <00:04:31.918>want <00:04:32.045>to <00:04:32.173>have <00:04:32.300>a <00:04:32.427>mathematical <00:04:32.554>proof.

85
00:04:34.255 --> 00:04:37.275
<00:04:34.255>On <00:04:34.395>the <00:04:34.534>other <00:04:34.675>hand, <00:04:34.815>we <00:04:34.955>are <00:04:35.094>just <00:04:35.235>about <00:04:35.375>to <00:04:35.515>detect <00:04:35.655>errors

86
00:04:37.275 --> 00:04:39.195
<00:04:37.275>through <00:04:38.674>executions

87
00:04:40.535 --> 00:04:43.155
<00:04:40.534>and <00:04:40.768>the <00:04:41.001>method <00:04:41.234>is <00:04:41.468>also <00:04:41.701>completely <00:04:41.934>different.

88
00:04:43.425 --> 00:04:45.115
<00:04:43.425>Here <00:04:43.625>we <00:04:43.825>write <00:04:44.025>coat, <00:04:44.225>on <00:04:44.425>the <00:04:44.625>other <00:04:44.825>hand,

89
00:04:45.175 --> 00:04:48.955
<00:04:45.175>we <00:04:45.375>write <00:04:45.575>formal <00:04:45.775>logical <00:04:45.975>formula <00:04:46.175>to <00:04:46.375>prove <00:04:46.575>it.

90
00:04:51.035 --> 00:04:52.635
<00:04:51.034>Software <00:04:51.501>verification <00:04:51.968>is <00:04:52.434>complete

91
00:04:54.715 --> 00:04:57.855
<00:04:54.715>and <00:04:54.855>software <00:04:54.995>testing <00:04:55.135>is <00:04:55.275>most, <00:04:55.415>in <00:04:55.555>most <00:04:55.695>of <00:04:55.835>the <00:04:55.975>cases <00:04:56.115>not.

92
00:04:58.195 --> 00:04:59.655
<00:04:58.195>And <00:04:58.523>also <00:04:58.852>the <00:04:59.180>error <00:04:59.508>coverage.

93
00:05:00.035 --> 00:05:01.575
<00:05:00.035>On <00:05:00.233>the <00:05:00.431>one <00:05:00.629>hand <00:05:00.827>you <00:05:01.025>find <00:05:01.223>the <00:05:01.421>errors.

94
00:05:01.575 --> 00:05:03.535
<00:05:01.575>On <00:05:01.808>the <00:05:02.041>other <00:05:02.275>hand, <00:05:02.508>you <00:05:02.741>really <00:05:02.974>guarantee

95
00:05:03.535 --> 00:05:04.815
<00:05:03.535>that <00:05:03.823>there <00:05:04.111>are <00:05:04.399>no <00:05:04.687>errors.

96
00:05:06.465 --> 00:05:07.565
<00:05:06.465>We <00:05:06.794>have <00:05:07.125>some <00:05:07.455>examples

97
00:05:08.305 --> 00:05:10.885
<00:05:08.305>and <00:05:08.480>one <00:05:08.655>of <00:05:08.830>them <00:05:09.005>are <00:05:09.180>core <00:05:09.355>calculus, <00:05:09.530>core <00:05:09.705>logic,

98
00:05:11.495 --> 00:05:14.525
<00:05:11.495>which <00:05:11.695>I <00:05:11.895>will <00:05:12.095>introduce <00:05:12.295>in <00:05:12.495>the <00:05:12.695>next <00:05:12.895>slide.

99
00:05:16.075 --> 00:05:18.295
<00:05:16.075>But <00:05:16.250>there <00:05:16.425>are <00:05:16.599>also <00:05:16.775>other <00:05:16.950>examples <00:05:17.125>like <00:05:17.300>model <00:05:17.474>checking

100
00:05:18.295 --> 00:05:20.655
<00:05:18.295>and <00:05:18.470>so <00:05:18.645>on, <00:05:18.820>which <00:05:18.995>are <00:05:19.170>widely <00:05:19.345>used <00:05:19.520>for <00:05:19.695>testing.

101
00:05:20.725 --> 00:05:22.375
<00:05:20.725>It's <00:05:21.005>clear <00:05:21.285>we <00:05:21.565>use <00:05:21.845>unit <00:05:22.125>testing

102
00:05:22.435 --> 00:05:24.815
<00:05:22.435>and <00:05:22.590>a <00:05:22.746>lot <00:05:22.901>of <00:05:23.057>other <00:05:23.212>tools <00:05:23.368>which <00:05:23.523>are <00:05:23.679>very <00:05:23.835>common.

103
00:05:26.805 --> 00:05:30.625
<00:05:26.805>Uh, <00:05:26.960>the <00:05:27.116>funny <00:05:27.271>fact <00:05:27.427>is <00:05:27.582>that <00:05:27.738>there <00:05:27.893>are <00:05:28.049>really <00:05:28.205>only

104
00:05:31.225 --> 00:05:32.225
<00:05:31.225>a <00:05:31.675>few <00:05:32.125>applications.

105
00:05:32.905 --> 00:05:34.745
<00:05:32.905>I <00:05:33.104>never <00:05:33.304>had <00:05:33.505>an <00:05:33.705>application <00:05:33.905>where <00:05:34.104>I <00:05:34.304>had

106
00:05:34.745 --> 00:05:35.985
<00:05:34.745>to <00:05:35.117>use <00:05:35.489>software <00:05:35.861>verification.

107
00:05:36.235 --> 00:05:37.985
<00:05:36.235>These <00:05:36.468>are <00:05:36.701>mostly <00:05:36.935>used <00:05:37.168>in <00:05:37.401>critical <00:05:37.635>systems,

108
00:05:38.405 --> 00:05:39.985
<00:05:38.405>but <00:05:38.638>for <00:05:38.871>software <00:05:39.104>testing <00:05:39.338>we <00:05:39.571>use <00:05:39.804>it

109
00:05:39.985 --> 00:05:41.265
<00:05:39.985>nearly <00:05:40.369>in <00:05:40.753>every <00:05:41.137>application.

110
00:05:41.425 --> 00:05:43.065
<00:05:41.425>I <00:05:41.658>never <00:05:41.891>had <00:05:42.125>an <00:05:42.358>application <00:05:42.591>without <00:05:42.825>tests.

111
00:05:43.845 --> 00:05:46.185
<00:05:43.845>And <00:05:44.000>if <00:05:44.156>there <00:05:44.311>were <00:05:44.467>no <00:05:44.622>tests, <00:05:44.778>actually <00:05:44.933>the <00:05:45.089>application <00:05:45.245>was

112
00:05:46.775 --> 00:05:48.185
<00:05:46.775>they're <00:05:47.028>thrown <00:05:47.282>away <00:05:47.536>in <00:05:47.790>the <00:05:48.044>end.

113
00:05:50.505 --> 00:05:53.445
<00:05:50.505>But <00:05:50.705>the <00:05:50.905>problem <00:05:51.105>with <00:05:51.305>software <00:05:51.505>verification <00:05:51.705>is <00:05:51.905>that

114
00:05:54.395 --> 00:05:56.565
<00:05:54.395>it's <00:05:54.550>really <00:05:54.706>complex <00:05:54.861>and <00:05:55.017>it <00:05:55.172>takes <00:05:55.328>a <00:05:55.483>lot <00:05:55.639>of <00:05:55.794>time.

115
00:05:56.745 --> 00:06:01.725
<00:05:56.745>So <00:05:56.885>in <00:05:57.025>most <00:05:57.165>cases <00:05:57.305>it <00:05:57.445>does <00:05:57.585>not <00:05:57.725>make <00:05:57.865>sense <00:05:58.005>to <00:05:58.145>really

116
00:06:02.695 --> 00:06:04.725
<00:06:02.695>write <00:06:03.161>validation <00:06:03.628>for <00:06:04.094>software.

117
00:06:07.075 --> 00:06:08.935
<00:06:07.075>So <00:06:07.354>an <00:06:07.635>introduction <00:06:07.914>to <00:06:08.195>our <00:06:08.474>logic

118
00:06:08.935 --> 00:06:10.935
<00:06:08.935>before <00:06:09.285>we <00:06:09.635>go <00:06:09.985>to <00:06:10.335>um,

119
00:06:11.165 --> 00:06:14.725
<00:06:11.165>real <00:06:11.445>world <00:06:11.725>example, <00:06:12.005>the <00:06:12.285>horror <00:06:12.565>logic.

120
00:06:15.625 --> 00:06:17.285
<00:06:15.625>Uh, <00:06:15.825>who <00:06:16.025>of <00:06:16.225>you <00:06:16.425>guys <00:06:16.625>know <00:06:16.825>it <00:06:17.025>already?

121
00:06:19.925 --> 00:06:23.455
<00:06:19.925>Okay, <00:06:20.100>only <00:06:20.275>a <00:06:20.450>few. <00:06:20.625>Few <00:06:20.800>and <00:06:20.975>only <00:06:21.150>two <00:06:21.325>more.

122
00:06:24.005 --> 00:06:27.415
<00:06:24.005>Yeah, <00:06:24.180>just <00:06:24.355>to <00:06:24.530>have <00:06:24.705>a <00:06:24.880>short <00:06:25.055>introduction <00:06:25.230>into <00:06:25.405>it.

123
00:06:27.635 --> 00:06:31.415
<00:06:27.635>Our <00:06:27.914>logic <00:06:28.195>consists <00:06:28.474>of <00:06:28.755>free <00:06:29.034>components.

124
00:06:32.885 --> 00:06:37.625
<00:06:32.885>We <00:06:33.060>have <00:06:33.235>the <00:06:33.409>precondition <00:06:33.585>as <00:06:33.760>you <00:06:33.935>see <00:06:34.110>with <00:06:34.284>P,

125
00:06:38.335 --> 00:06:42.065
<00:06:38.335>then <00:06:38.451>we <00:06:38.568>have <00:06:38.685>C, <00:06:38.801>this <00:06:38.918>is <00:06:39.034>the <00:06:39.151>code <00:06:39.268>which <00:06:39.385>has <00:06:39.501>to <00:06:39.618>be <00:06:39.734>executed.

126
00:06:43.285 --> 00:06:47.025
<00:06:43.284>And <00:06:43.440>then <00:06:43.596>we <00:06:43.751>have <00:06:43.907>the <00:06:44.062>Q <00:06:44.218>as <00:06:44.373>a <00:06:44.529>post <00:06:44.684>condition.

127
00:06:49.005 --> 00:06:53.985
<00:06:49.005>And <00:06:49.121>in <00:06:49.238>the <00:06:49.355>end <00:06:49.471>this <00:06:49.588>means <00:06:49.705>that <00:06:49.821>if <00:06:49.938>we <00:06:50.055>execute <00:06:50.171>the <00:06:50.288>code <00:06:50.405>C

128
00:06:54.625 --> 00:06:58.905
<00:06:54.625>starting <00:06:54.741>from <00:06:54.858>a <00:06:54.975>valid <00:06:55.091>point <00:06:55.208>P, <00:06:55.325>then <00:06:55.441>we <00:06:55.558>have <00:06:55.675>to <00:06:55.791>be <00:06:55.908>on <00:06:56.025>a

129
00:06:59.565 --> 00:07:00.745
<00:06:59.565>post-condition <00:07:00.627>queue.

130
00:07:03.275 --> 00:07:05.855
<00:07:03.275>If <00:07:03.430>we <00:07:03.586>look <00:07:03.741>into <00:07:03.897>it <00:07:04.052>with <00:07:04.208>a <00:07:04.363>short <00:07:04.519>example, <00:07:04.674>this

131
00:07:06.575 --> 00:07:11.145
<00:07:06.575>swapping <00:07:06.750>values, <00:07:06.925>like <00:07:07.099>here <00:07:07.275>you <00:07:07.450>see <00:07:07.625>we <00:07:07.800>have, <00:07:07.974>um,

132
00:07:12.715 --> 00:07:15.135
<00:07:12.715>the <00:07:12.994>beginning <00:07:13.275>defined <00:07:13.554>uh, <00:07:13.835>Java <00:07:14.114>method

133
00:07:15.705 --> 00:07:17.575
<00:07:15.705>where <00:07:15.938>you <00:07:16.171>see <00:07:16.405>two <00:07:16.638>variables <00:07:16.871>in <00:07:17.104>it.

134
00:07:17.715 --> 00:07:20.335
<00:07:17.715>And <00:07:17.890>in <00:07:18.065>this <00:07:18.239>variable, <00:07:18.414>in <00:07:18.590>this <00:07:18.765>method, <00:07:18.940>we <00:07:19.114>have

135
00:07:21.055 --> 00:07:22.215
<00:07:21.055>a <00:07:21.577>temporary <00:07:22.099>variable

136
00:07:22.835 --> 00:07:26.485
<00:07:22.835>and <00:07:22.974>then <00:07:23.114>we <00:07:23.255>do <00:07:23.395>the <00:07:23.534>switch <00:07:23.674>that <00:07:23.815>this <00:07:23.955>method <00:07:24.094>is <00:07:24.234>correct.

137
00:07:27.325 --> 00:07:29.885
<00:07:27.325>I <00:07:27.480>think <00:07:27.636>that <00:07:27.791>it's <00:07:27.947>quite <00:07:28.102>obvious <00:07:28.258>if <00:07:28.413>we <00:07:28.569>map <00:07:28.724>it

138
00:07:29.885 --> 00:07:31.925
<00:07:29.885>to <00:07:30.060>the <00:07:30.235>hard <00:07:30.409>calculus, <00:07:30.585>it <00:07:30.760>would <00:07:30.935>look <00:07:31.110>like <00:07:31.284>this

139
00:07:32.475 --> 00:07:37.005
<00:07:32.475>that <00:07:32.615>we <00:07:32.755>define <00:07:32.895>the <00:07:33.035>precondition <00:07:33.175>with <00:07:33.315>A, <00:07:33.455>is <00:07:33.595>the <00:07:33.735>assignment <00:07:33.875>A

140
00:07:37.265 --> 00:07:38.805
<00:07:37.265>and <00:07:37.542>B, <00:07:37.819>is <00:07:38.096>it <00:07:38.373>assignment <00:07:38.651>B?

141
00:07:38.805 --> 00:07:42.725
<00:07:38.805>This <00:07:38.921>has <00:07:39.038>to <00:07:39.155>be <00:07:39.271>true. <00:07:39.388>Then <00:07:39.505>the <00:07:39.621>code <00:07:39.738>which <00:07:39.855>we <00:07:39.971>have <00:07:40.088>to <00:07:40.205>apply

142
00:07:43.625 --> 00:07:46.055
<00:07:43.625>is <00:07:43.975>also <00:07:44.325>very, <00:07:44.675>uh, <00:07:45.025>easy.

143
00:07:46.875 --> 00:07:50.575
<00:07:46.875>And <00:07:47.002>the <00:07:47.129>past <00:07:47.256>condition <00:07:47.384>will <00:07:47.511>be <00:07:47.638>that <00:07:47.765>A <00:07:47.893>is <00:07:48.020>the <00:07:48.147>assignment <00:07:48.275>B

144
00:07:50.575 --> 00:07:52.055
<00:07:50.575>and <00:07:50.796>B <00:07:51.019>has <00:07:51.241>the <00:07:51.463>assignment <00:07:51.685>of <00:07:51.907>a

145
00:07:53.745 --> 00:07:55.805
<00:07:53.745>and <00:07:53.945>that <00:07:54.145>this <00:07:54.345>works <00:07:54.545>correct <00:07:54.745>is <00:07:54.945>quite <00:07:55.145>obvious.

146
00:07:55.865 --> 00:07:59.085
<00:07:55.865>But <00:07:56.040>what <00:07:56.215>do <00:07:56.390>we <00:07:56.565>do <00:07:56.740>with <00:07:56.915>more <00:07:57.090>complex <00:07:57.265>stuff?

147
00:08:04.245 --> 00:08:06.505
<00:08:04.245>And <00:08:04.400>if <00:08:04.556>we <00:08:04.711>have <00:08:04.867>more <00:08:05.022>complex <00:08:05.178>stuff, <00:08:05.333>then <00:08:05.489>we <00:08:05.645>have

148
00:08:06.505 --> 00:08:09.505
<00:08:06.505>to <00:08:06.680>break <00:08:06.855>down <00:08:07.030>the <00:08:07.205>complex <00:08:07.380>problems <00:08:07.555>into <00:08:07.730>simple <00:08:07.905>parts,

149
00:08:09.675 --> 00:08:11.345
<00:08:09.675>which <00:08:10.141>are <00:08:10.608>called <00:08:11.075>axioms.

150
00:08:11.835 --> 00:08:13.705
<00:08:11.835>These <00:08:12.301>axioms <00:08:12.768>are <00:08:13.234>statements.

151
00:08:13.705 --> 00:08:15.865
<00:08:13.705>They're <00:08:13.938>accepted <00:08:14.171>as <00:08:14.405>true <00:08:14.638>without <00:08:14.871>the <00:08:15.104>proof.

152
00:08:17.335 --> 00:08:19.795
<00:08:17.335>Now <00:08:17.534>I <00:08:17.734>will <00:08:17.935>just <00:08:18.135>introduce <00:08:18.335>a <00:08:18.534>few <00:08:18.734>axioms

153
00:08:19.795 --> 00:08:23.075
<00:08:19.795>before <00:08:20.028>we <00:08:20.261>go <00:08:20.495>to <00:08:20.728>the <00:08:20.961>Java <00:08:21.195>code.

154
00:08:24.355 --> 00:08:26.295
<00:08:24.355>The <00:08:24.588>first <00:08:24.821>one <00:08:25.055>is <00:08:25.288>the <00:08:25.521>assignment <00:08:25.755>axiom.

155
00:08:26.845 --> 00:08:31.695
<00:08:26.845>Here <00:08:27.078>we <00:08:27.311>see <00:08:27.545>that <00:08:27.778>we <00:08:28.011>are <00:08:28.245>starting

156
00:08:31.765 --> 00:08:36.135
<00:08:31.765>from <00:08:31.920>a <00:08:32.076>post <00:08:32.231>condition <00:08:32.387>where <00:08:32.542>Y <00:08:32.698>is <00:08:32.853>greater <00:08:33.009>than <00:08:33.164>five

157
00:08:37.525 --> 00:08:39.145
<00:08:37.525>and <00:08:37.875>the <00:08:38.225>assignment <00:08:38.574>is <00:08:38.924>Y

158
00:08:40.905 --> 00:08:42.955
<00:08:40.905>gets <00:08:41.184>a <00:08:41.464>value <00:08:41.745>x <00:08:42.025>plus <00:08:42.304>one.

159
00:08:45.385 --> 00:08:49.805
<00:08:45.385>And <00:08:45.540>with <00:08:45.696>this <00:08:45.851>assignment <00:08:46.007>exum, <00:08:46.162>we <00:08:46.318>replace <00:08:46.473>all <00:08:46.629>the <00:08:46.785>X

160
00:08:50.075 --> 00:08:53.455
<00:08:50.075>with <00:08:50.541>the <00:08:51.008>expression <00:08:51.475>E.

161
00:08:53.995 --> 00:08:57.325
<00:08:53.995>So <00:08:54.150>we <00:08:54.306>get <00:08:54.461>X <00:08:54.617>plus <00:08:54.772>one <00:08:54.928>is <00:08:55.083>greater <00:08:55.239>than <00:08:55.395>five,

162
00:08:58.635 --> 00:09:03.215
<00:08:58.635>and <00:08:58.810>this <00:08:58.985>we <00:08:59.160>can <00:08:59.335>be, <00:08:59.510>this <00:08:59.685>can <00:08:59.860>be, <00:09:00.035>uh,

163
00:09:03.215 --> 00:09:05.335
<00:09:03.215>translate <00:09:03.448>to <00:09:03.681>X <00:09:03.915>is <00:09:04.148>greater <00:09:04.381>than <00:09:04.615>four.

164
00:09:05.635 --> 00:09:08.215
<00:09:05.635>And <00:09:05.868>then <00:09:06.101>you <00:09:06.335>see <00:09:06.568>that <00:09:06.801>this <00:09:07.035>holds

165
00:09:08.215 --> 00:09:09.615
<00:09:08.215>that <00:09:08.467>X <00:09:08.719>is <00:09:08.971>greater <00:09:09.223>than <00:09:09.475>four.

166
00:09:09.615 --> 00:09:14.215
<00:09:09.615>And <00:09:09.742>if <00:09:09.869>you <00:09:09.996>assign <00:09:10.124>if <00:09:10.251>plus <00:09:10.378>one <00:09:10.505>then <00:09:10.633>x, <00:09:10.760>then <00:09:10.887>Y <00:09:11.015>has

167
00:09:14.215 --> 00:09:15.935
<00:09:14.215>to <00:09:14.565>be <00:09:14.915>greater <00:09:15.265>than <00:09:15.615>five.

168
00:09:17.255 --> 00:09:21.635
<00:09:17.255>And <00:09:17.382>this <00:09:17.509>would <00:09:17.636>be <00:09:17.764>an <00:09:17.891>axiom <00:09:18.018>that <00:09:18.145>we <00:09:18.273>can <00:09:18.400>just, <00:09:18.527>uh, <00:09:18.655>accept

169
00:09:21.695 --> 00:09:25.225
<00:09:21.695>as <00:09:21.895>true <00:09:22.095>without <00:09:22.295>a <00:09:22.495>proof <00:09:22.695>in <00:09:22.895>validating <00:09:23.095>software.

170
00:09:25.915 --> 00:09:29.105
<00:09:25.915>There <00:09:26.089>are <00:09:26.265>other <00:09:26.439>axioms <00:09:26.615>like <00:09:26.790>the <00:09:26.964>rule <00:09:27.140>of <00:09:27.314>composition

171
00:09:31.565 --> 00:09:35.825
<00:09:31.565>in <00:09:31.692>this <00:09:31.819>sense <00:09:31.946>executing <00:09:32.074>C <00:09:32.201>one <00:09:32.328>from <00:09:32.455>a <00:09:32.583>state <00:09:32.710>where <00:09:32.837>P <00:09:32.965>holds

172
00:09:35.925 --> 00:09:38.545
<00:09:35.925>and <00:09:36.125>result <00:09:36.324>in <00:09:36.525>a <00:09:36.724>state <00:09:36.925>where <00:09:37.125>co <00:09:37.324>holds

173
00:09:39.445 --> 00:09:42.465
<00:09:39.445>and <00:09:39.645>executing <00:09:39.845>afterwards <00:09:40.045>C <00:09:40.245>two <00:09:40.445>from <00:09:40.645>a <00:09:40.845>state

174
00:09:43.425 --> 00:09:46.175
<00:09:43.425>where <00:09:43.580>co <00:09:43.736>holds <00:09:43.891>result <00:09:44.047>in <00:09:44.202>a <00:09:44.358>state <00:09:44.513>where <00:09:44.669>R <00:09:44.824>holds.

175
00:09:48.665 --> 00:09:52.285
<00:09:48.665>And <00:09:48.805>then <00:09:48.944>you <00:09:49.084>can <00:09:49.224>compose <00:09:49.365>them <00:09:49.505>into <00:09:49.645>executing <00:09:49.785>both <00:09:49.925>C <00:09:50.064>one

176
00:09:52.285 --> 00:09:55.325
<00:09:52.285>and <00:09:52.459>C <00:09:52.635>two <00:09:52.810>from <00:09:52.985>a <00:09:53.160>state <00:09:53.334>where <00:09:53.510>P <00:09:53.685>holds

177
00:09:55.825 --> 00:09:58.285
<00:09:55.825>and <00:09:56.000>it'll <00:09:56.175>result <00:09:56.350>in <00:09:56.525>a <00:09:56.700>state <00:09:56.875>where <00:09:57.050>R <00:09:57.225>holds.

178
00:09:58.825 --> 00:10:00.045
<00:09:58.825>So <00:09:59.099>just <00:09:59.374>putting <00:09:59.648>them <00:09:59.923>together.

179
00:10:01.945 --> 00:10:04.245
<00:10:01.945>And <00:10:02.120>the <00:10:02.295>third <00:10:02.470>axiom <00:10:02.645>I <00:10:02.820>want <00:10:02.995>to <00:10:03.170>introduce <00:10:03.345>is

180
00:10:05.025 --> 00:10:06.045
<00:10:05.025>the <00:10:05.483>conditional <00:10:05.943>rule.

181
00:10:08.245 --> 00:10:11.585
<00:10:08.245>Here <00:10:08.595>you <00:10:08.945>see <00:10:09.295>that, <00:10:09.645>uh,

182
00:10:12.875 --> 00:10:17.175
<00:10:12.875>we <00:10:13.015>can <00:10:13.155>just <00:10:13.295>break <00:10:13.435>down <00:10:13.575>also <00:10:13.715>this <00:10:13.855>into <00:10:13.995>two <00:10:14.135>parts <00:10:14.275>where

183
00:10:18.015 --> 00:10:19.575
<00:10:18.015>independently <00:10:18.295>from <00:10:18.574>B, <00:10:18.855>if <00:10:19.135>it's <00:10:19.415>true

184
00:10:19.575 --> 00:10:23.935
<00:10:19.575>or <00:10:19.730>not, <00:10:19.886>that <00:10:20.041>the <00:10:20.197>post <00:10:20.352>condition <00:10:20.508>will <00:10:20.663>hold <00:10:20.819>with <00:10:20.975>Q.

185
00:10:24.395 --> 00:10:27.935
<00:10:24.395>So <00:10:24.522>it's <00:10:24.649>independently <00:10:24.776>if <00:10:24.904>B <00:10:25.031>is <00:10:25.158>true <00:10:25.285>and <00:10:25.413>you <00:10:25.540>execute <00:10:25.667>C <00:10:25.795>one

186
00:10:27.935 --> 00:10:31.735
<00:10:27.935>or <00:10:28.042>P <00:10:28.150>is <00:10:28.258>fault <00:10:28.365>and <00:10:28.473>you <00:10:28.581>execute <00:10:28.688>C <00:10:28.796>two, <00:10:28.904>we <00:10:29.011>need <00:10:29.119>to <00:10:29.227>have <00:10:29.334>Q

187
00:10:31.995 --> 00:10:33.295
<00:10:31.995>and <00:10:32.287>this <00:10:32.579>holds <00:10:32.872>as <00:10:33.165>well.

188
00:10:33.435 --> 00:10:36.255
<00:10:33.435>And <00:10:33.551>this <00:10:33.668>can <00:10:33.785>be <00:10:33.901>seen <00:10:34.018>also <00:10:34.135>as <00:10:34.251>a <00:10:34.368>true <00:10:34.484>value <00:10:34.601>if <00:10:34.718>you <00:10:34.834>can

189
00:10:36.825 --> 00:10:38.855
<00:10:36.825>break <00:10:37.105>a <00:10:37.385>if <00:10:37.665>clause <00:10:37.945>like <00:10:38.225>this

190
00:10:42.425 --> 00:10:45.045
<00:10:42.425>and <00:10:42.625>how <00:10:42.824>this <00:10:43.025>all <00:10:43.224>gets <00:10:43.425>to <00:10:43.625>approve <00:10:43.824>together.

191
00:10:47.145 --> 00:10:51.205
<00:10:47.145>In <00:10:47.300>the <00:10:47.456>end, <00:10:47.611>it's <00:10:47.767>about <00:10:47.922>we <00:10:48.078>have <00:10:48.233>a <00:10:48.389>starting <00:10:48.545>point.

192
00:10:51.505 --> 00:10:53.845
<00:10:51.505>You <00:10:51.680>can <00:10:51.855>see <00:10:52.030>this, <00:10:52.205>the <00:10:52.380>beginning <00:10:52.555>of <00:10:52.730>a <00:10:52.905>method

193
00:10:54.025 --> 00:10:57.305
<00:10:54.025>and <00:10:54.305>an <00:10:54.584>endpoint <00:10:54.865>queue <00:10:55.145>the <00:10:55.425>result

194
00:10:57.305 --> 00:10:59.505
<00:10:57.305>of <00:10:57.479>a <00:10:57.655>method <00:10:57.829>like <00:10:58.005>a <00:10:58.180>return <00:10:58.354>value <00:10:58.530>may <00:10:58.704>be.

195
00:11:00.475 --> 00:11:03.255
<00:11:00.475>And <00:11:00.630>in <00:11:00.786>this <00:11:00.941>we <00:11:01.097>have <00:11:01.252>different <00:11:01.408>statements <00:11:01.563>which <00:11:01.719>are <00:11:01.875>just

196
00:11:03.615 --> 00:11:04.855
<00:11:03.615>executed <00:11:03.894>C <00:11:04.173>one <00:11:04.452>to <00:11:04.731>CN.

197
00:11:06.475 --> 00:11:09.765
<00:11:06.475>Here <00:11:06.650>we <00:11:06.825>have <00:11:07.000>to <00:11:07.175>go <00:11:07.350>backwards <00:11:07.525>reasoning <00:11:07.700>where <00:11:07.875>see

198
00:11:09.765 --> 00:11:12.085
<00:11:09.765>that <00:11:09.965>we <00:11:10.165>start <00:11:10.365>from <00:11:10.564>the <00:11:10.765>post-condition <00:11:10.965>by <00:11:11.165>defining

199
00:11:15.125 --> 00:11:18.655
<00:11:15.125>and <00:11:15.325>then <00:11:15.525>apply <00:11:15.725>first <00:11:15.925>to <00:11:16.125>C <00:11:16.325>end <00:11:16.525>step

200
00:11:19.155 --> 00:11:22.105
<00:11:19.155>to <00:11:19.388>get <00:11:19.621>the <00:11:19.855>pn <00:11:20.088>the <00:11:20.321>first, <00:11:20.555>uh,

201
00:11:22.445 --> 00:11:25.945
<00:11:22.445>the <00:11:22.600>first <00:11:22.756>precondition <00:11:22.911>at <00:11:23.067>this <00:11:23.222>precondition <00:11:23.378>will <00:11:23.533>be <00:11:23.689>then <00:11:23.845>the

202
00:11:25.945 --> 00:11:28.515
<00:11:25.945>post-condition <00:11:26.295>of <00:11:26.645>the <00:11:26.995>next <00:11:27.345>step

203
00:11:28.535 --> 00:11:32.995
<00:11:28.535>and <00:11:28.651>so <00:11:28.768>on <00:11:28.885>until <00:11:29.001>we <00:11:29.118>have <00:11:29.235>no <00:11:29.351>code <00:11:29.468>code <00:11:29.584>to <00:11:29.701>execute <00:11:29.818>any <00:11:29.935>longer.

204
00:11:38.795 --> 00:11:41.655
<00:11:38.795>And <00:11:38.935>how <00:11:39.074>is <00:11:39.214>it <00:11:39.354>done <00:11:39.495>with <00:11:39.635>state <00:11:39.775>of <00:11:39.915>the <00:11:40.055>art <00:11:40.194>verification?

205
00:11:41.975 --> 00:11:46.335
<00:11:41.975>Actually <00:11:42.130>what <00:11:42.286>is <00:11:42.441>done <00:11:42.597>today, <00:11:42.752>we <00:11:42.908>have <00:11:43.063>today, <00:11:43.219>uh, <00:11:43.375>software

206
00:11:46.395 --> 00:11:47.575
<00:11:46.395>for <00:11:46.926>validating <00:11:47.457>code.

207
00:11:48.205 --> 00:11:50.895
<00:11:48.205>This <00:11:48.438>code <00:11:48.671>is <00:11:48.905>mostly <00:11:49.138>combined <00:11:49.371>formal <00:11:49.605>methods

208
00:11:50.955 --> 00:11:52.135
<00:11:50.955>and <00:11:51.486>model-based <00:11:52.017>techniques.

209
00:11:54.115 --> 00:11:55.495
<00:11:54.115>And <00:11:54.736>here, <00:11:55.357>uh,

210
00:11:55.605 --> 00:11:58.935
<00:11:55.605>it's <00:11:55.760>like <00:11:55.916>also <00:11:56.071>hard <00:11:56.227>calculus <00:11:56.382>is <00:11:56.538>really <00:11:56.693>used <00:11:56.849>a <00:11:57.005>lot.

211
00:12:00.915 --> 00:12:03.655
<00:12:00.915>We <00:12:01.115>have <00:12:01.314>tools <00:12:01.515>like <00:12:01.714>SMT <00:12:01.915>solvers, <00:12:02.115>model <00:12:02.314>checkers

212
00:12:04.075 --> 00:12:05.815
<00:12:04.075>and <00:12:04.775>peer <00:12:05.475>improvers.

213
00:12:06.085 --> 00:12:07.975
<00:12:06.085>Just <00:12:06.285>a <00:12:06.485>few <00:12:06.685>of <00:12:06.885>them <00:12:07.085>are <00:12:07.285>listed <00:12:07.485>here.

214
00:12:09.525 --> 00:12:12.065
<00:12:09.525>And <00:12:09.699>this <00:12:09.875>stuff <00:12:10.050>is <00:12:10.225>widely <00:12:10.400>used <00:12:10.574>in <00:12:10.750>critical <00:12:10.925>systems

215
00:12:13.345 --> 00:12:15.195
<00:12:13.345>like <00:12:13.695>medical <00:12:14.045>software <00:12:14.395>and <00:12:14.745>aerospace.

216
00:12:16.635 --> 00:12:17.775
<00:12:16.635>Why <00:12:16.891>is <00:12:17.148>this <00:12:17.404>the <00:12:17.661>case?

217
00:12:17.775 --> 00:12:19.615
<00:12:17.775>Because <00:12:18.055>the <00:12:18.334>effort, <00:12:18.615>the <00:12:18.895>manual <00:12:19.175>effort

218
00:12:19.635 --> 00:12:21.135
<00:12:19.635>for <00:12:20.085>defining <00:12:20.535>these <00:12:20.985>preconditions

219
00:12:21.135 --> 00:12:23.095
<00:12:21.135>and <00:12:21.485>post-condition <00:12:21.835>is <00:12:22.185>still <00:12:22.535>high.

220
00:12:24.425 --> 00:12:27.925
<00:12:24.425>But <00:12:24.525>if <00:12:24.625>we <00:12:24.724>can <00:12:24.824>get <00:12:24.925>to <00:12:25.025>a <00:12:25.125>point <00:12:25.224>where <00:12:25.324>AI <00:12:25.425>does <00:12:25.525>this <00:12:25.625>work <00:12:25.724>for <00:12:25.824>us,

221
00:12:28.675 --> 00:12:31.965
<00:12:28.675>then <00:12:28.814>it <00:12:28.954>might <00:12:29.094>not <00:12:29.234>be <00:12:29.375>the <00:12:29.515>case <00:12:29.655>that <00:12:29.795>we <00:12:29.935>have <00:12:30.074>to

222
00:12:32.865 --> 00:12:33.965
<00:12:32.865>do <00:12:33.112>testing <00:12:33.360>the <00:12:33.607>whole <00:12:33.855>time.

223
00:12:33.965 --> 00:12:36.645
<00:12:33.965>Maybe <00:12:34.140>we <00:12:34.315>can <00:12:34.490>also <00:12:34.665>think <00:12:34.840>sometimes <00:12:35.015>about <00:12:35.190>welding <00:12:35.365>software.

224
00:12:38.745 --> 00:12:40.275
<00:12:38.745>Here <00:12:39.089>I <00:12:39.433>have <00:12:39.777>an <00:12:40.122>example

225
00:12:40.905 --> 00:12:44.465
<00:12:40.905>with <00:12:41.255>open <00:12:41.605>GMEL <00:12:41.954>with <00:12:42.305>Java.

226
00:12:45.135 --> 00:12:49.145
<00:12:45.135>This <00:12:45.251>is <00:12:45.368>a <00:12:45.485>tool <00:12:45.601>where <00:12:45.718>it's <00:12:45.835>a <00:12:45.951>tool <00:12:46.068>for <00:12:46.185>verifying <00:12:46.301>uh, <00:12:46.418>Java <00:12:46.535>code

227
00:12:50.005 --> 00:12:54.615
<00:12:50.005>and <00:12:50.205>it <00:12:50.405>checks <00:12:50.605>code <00:12:50.805>according <00:12:51.005>to <00:12:51.205>annotations <00:12:51.405>open.

228
00:12:54.615 --> 00:12:58.095
<00:12:54.615>Jamie <00:12:54.815>l <00:12:55.015>also <00:12:55.215>uses <00:12:55.415>her <00:12:55.615>calcu, <00:12:55.815>her <00:12:56.015>logic

229
00:12:58.515 --> 00:13:00.015
<00:12:58.515>for <00:12:59.189>his <00:12:59.865>validation.

230
00:13:02.285 --> 00:13:03.505
<00:13:02.285>How <00:13:02.559>does <00:13:02.834>this <00:13:03.108>look <00:13:03.383>like?

231
00:13:06.865 --> 00:13:10.715
<00:13:06.865>Here <00:13:07.020>I <00:13:07.176>have <00:13:07.331>a <00:13:07.487>code <00:13:07.642>slip <00:13:07.798>it <00:13:07.953>a <00:13:08.109>binary <00:13:08.265>search.

232
00:13:12.655 --> 00:13:17.005
<00:13:12.655>It's <00:13:12.888>a <00:13:13.121>very <00:13:13.355>easy, <00:13:13.588>uh, <00:13:13.821>search <00:13:14.055>actually

233
00:13:17.005 --> 00:13:19.445
<00:13:17.005>where <00:13:17.205>you <00:13:17.405>have <00:13:17.605>a <00:13:17.805>sorted <00:13:18.005>array <00:13:18.205>as <00:13:18.405>input

234
00:13:19.905 --> 00:13:21.045
<00:13:19.905>and <00:13:20.110>you <00:13:20.315>have <00:13:20.520>an <00:13:20.725>in <00:13:20.930>value

235
00:13:21.545 --> 00:13:25.405
<00:13:21.545>and <00:13:21.700>in <00:13:21.856>the <00:13:22.011>end <00:13:22.167>you <00:13:22.322>want <00:13:22.478>to <00:13:22.633>have <00:13:22.789>the <00:13:22.944>index

236
00:13:25.465 --> 00:13:27.485
<00:13:25.465>of <00:13:25.745>the <00:13:26.025>value <00:13:26.305>you're <00:13:26.585>looking <00:13:26.865>for.

237
00:13:27.985 --> 00:13:29.165
<00:13:27.985>If <00:13:28.250>the <00:13:28.516>index <00:13:28.781>is <00:13:29.047>not,

238
00:13:29.185 --> 00:13:31.245
<00:13:29.185>if <00:13:29.340>the <00:13:29.496>value <00:13:29.651>is <00:13:29.807>not <00:13:29.962>available <00:13:30.118>in <00:13:30.273>the <00:13:30.429>sorted <00:13:30.584>array,

239
00:13:31.625 --> 00:13:34.485
<00:13:31.625>you <00:13:31.905>will <00:13:32.185>get <00:13:32.465>a <00:13:32.745>return <00:13:33.025>value,

240
00:13:35.345 --> 00:13:37.795
<00:13:35.345>uh, <00:13:36.045>minus <00:13:36.745>one.

241
00:13:39.975 --> 00:13:42.995
<00:13:39.975>So <00:13:40.208>how <00:13:40.441>this <00:13:40.675>works <00:13:40.908>just <00:13:41.141>very <00:13:41.375>short.

242
00:13:43.575 --> 00:13:48.265
<00:13:43.575>In <00:13:43.702>the <00:13:43.829>beginning <00:13:43.956>we <00:13:44.084>just <00:13:44.211>checked <00:13:44.338>if <00:13:44.465>the <00:13:44.593>search <00:13:44.720>array <00:13:44.847>is <00:13:44.975>um,

243
00:13:49.435 --> 00:13:53.295
<00:13:49.435>empty <00:13:49.574>or <00:13:49.714>no, <00:13:49.854>sorry, <00:13:49.994>we <00:13:50.135>check <00:13:50.275>if <00:13:50.415>the <00:13:50.555>value <00:13:50.694>is <00:13:50.834>uh,

244
00:13:53.465 --> 00:13:57.015
<00:13:53.465>lower <00:13:53.620>than <00:13:53.776>the <00:13:53.931>first <00:13:54.087>value <00:13:54.242>in <00:13:54.398>the <00:13:54.553>search <00:13:54.709>or <00:13:54.865>higher.

245
00:13:57.835 --> 00:14:00.415
<00:13:57.835>If <00:13:57.962>this <00:13:58.089>is <00:13:58.216>the <00:13:58.344>case, <00:13:58.471>then <00:13:58.598>the <00:13:58.725>value <00:13:58.853>is <00:13:58.980>not <00:13:59.107>in <00:13:59.235>just

246
00:14:00.415 --> 00:14:01.495
<00:14:00.415>because <00:14:00.739>it's <00:14:01.063>sorted <00:14:01.387>already.

247
00:14:02.985 --> 00:14:04.645
<00:14:02.985>And <00:14:03.185>then <00:14:03.385>we <00:14:03.585>go <00:14:03.785>into <00:14:03.985>a <00:14:04.185>wire <00:14:04.385>loop

248
00:14:04.645 --> 00:14:06.965
<00:14:04.645>and <00:14:04.925>then <00:14:05.204>we <00:14:05.485>check <00:14:05.765>there, <00:14:06.045>um,

249
00:14:09.205 --> 00:14:12.715
<00:14:09.205>every <00:14:09.405>time <00:14:09.605>we <00:14:09.805>hal <00:14:10.005>the <00:14:10.205>binary <00:14:10.405>tree <00:14:10.605>actually,

250
00:14:13.175 --> 00:14:15.155
<00:14:13.175>and <00:14:13.314>then <00:14:13.454>we <00:14:13.594>check <00:14:13.734>if <00:14:13.875>we <00:14:14.015>find <00:14:14.155>the <00:14:14.295>value <00:14:14.435>or <00:14:14.574>not.

251
00:14:15.175 --> 00:14:17.955
<00:14:15.175>We <00:14:15.349>do <00:14:15.525>the <00:14:15.699>do <00:14:15.875>this <00:14:16.050>until <00:14:16.224>the <00:14:16.400>lower <00:14:16.574>value

252
00:14:17.955 --> 00:14:19.315
<00:14:17.955>and <00:14:18.199>the <00:14:18.444>higher <00:14:18.689>value <00:14:18.934>come <00:14:19.179>together.

253
00:14:19.815 --> 00:14:22.835
<00:14:19.815>If <00:14:19.970>we <00:14:20.126>find <00:14:20.281>the <00:14:20.437>value, <00:14:20.592>then <00:14:20.748>we <00:14:20.903>return <00:14:21.059>the <00:14:21.215>index.

254
00:14:22.935 --> 00:14:25.595
<00:14:22.935>If <00:14:23.090>not, <00:14:23.246>then <00:14:23.401>we <00:14:23.557>return <00:14:23.712>in <00:14:23.868>the <00:14:24.023>end <00:14:24.179>minus <00:14:24.334>one.

255
00:14:27.665 --> 00:14:30.725
<00:14:27.665>How <00:14:27.805>would <00:14:27.944>a <00:14:28.084>validation <00:14:28.224>of <00:14:28.365>this <00:14:28.505>this <00:14:28.645>could <00:14:28.785>code <00:14:28.925>look <00:14:29.064>like?

256
00:14:31.675 --> 00:14:34.535
<00:14:31.675>If <00:14:31.814>we <00:14:31.954>have <00:14:32.094>to <00:14:32.234>write <00:14:32.375>this <00:14:32.515>on <00:14:32.655>our <00:14:32.795>own <00:14:32.935>with <00:14:33.074>Java?

257
00:14:34.915 --> 00:14:37.295
<00:14:34.915>Uh, <00:14:35.115>open <00:14:35.314>JMEL, <00:14:35.515>it <00:14:35.714>would <00:14:35.915>look <00:14:36.115>like <00:14:36.314>this.

258
00:14:37.475 --> 00:14:41.725
<00:14:37.475>As <00:14:37.825>you <00:14:38.175>see, <00:14:38.525>it's <00:14:38.875>very

259
00:14:43.005 --> 00:14:44.645
<00:14:43.005>actually <00:14:43.180>you <00:14:43.355>have <00:14:43.530>to <00:14:43.705>write <00:14:43.880>as <00:14:44.055>much <00:14:44.230>code <00:14:44.405>as

260
00:14:45.785 --> 00:14:49.125
<00:14:45.785>as <00:14:45.959>much <00:14:46.135>ver <00:14:46.310>verification <00:14:46.485>code, <00:14:46.660>a <00:14:46.834>validation <00:14:47.010>code <00:14:47.185>as

261
00:14:50.085 --> 00:14:52.725
<00:14:50.085>algorithm <00:14:50.785>code, <00:14:51.485>sorry.

262
00:14:58.965 --> 00:15:03.065
<00:14:58.965>But <00:14:59.105>what <00:14:59.245>we <00:14:59.385>see <00:14:59.525>here <00:14:59.665>are <00:14:59.805>the <00:14:59.945>requires <00:15:00.085>annotations <00:15:00.225>are <00:15:00.365>the

263
00:15:03.065 --> 00:15:05.825
<00:15:03.065>preconditions <00:15:03.265>and <00:15:03.465>the <00:15:03.665>insurers <00:15:03.865>are <00:15:04.065>the <00:15:04.265>post <00:15:04.465>conditions.

264
00:15:07.575 --> 00:15:10.155
<00:15:07.575>And <00:15:07.855>also <00:15:08.135>as <00:15:08.415>you <00:15:08.695>can <00:15:08.975>see,

265
00:15:10.455 --> 00:15:12.955
<00:15:10.455>the <00:15:10.595>first <00:15:10.735>one <00:15:10.875>just <00:15:11.015>says <00:15:11.155>if <00:15:11.295>the <00:15:11.435>sort <00:15:11.575>array <00:15:11.715>is <00:15:11.855>now

266
00:15:13.025 --> 00:15:15.835
<00:15:13.025>that <00:15:13.141>the <00:15:13.258>length <00:15:13.375>of <00:15:13.491>the <00:15:13.608>array <00:15:13.725>has <00:15:13.841>to <00:15:13.958>be <00:15:14.074>greater <00:15:14.191>than <00:15:14.308>one, <00:15:14.425>uh,

267
00:15:15.835 --> 00:15:19.675
<00:15:15.835>greater <00:15:15.990>than <00:15:16.146>zero, <00:15:16.301>and <00:15:16.457>the <00:15:16.612>max <00:15:16.768>length <00:15:16.923>of <00:15:17.079>the <00:15:17.235>array

268
00:15:20.775 --> 00:15:23.195
<00:15:20.775>is <00:15:20.975>allowed <00:15:21.175>to <00:15:21.375>be <00:15:21.574>greater <00:15:21.775>at <00:15:21.975>not <00:15:22.175>greater,

269
00:15:23.325 --> 00:15:26.315
<00:15:23.325>lower <00:15:23.558>than <00:15:23.791>intergen <00:15:24.025>max <00:15:24.258>value, <00:15:24.491>that's <00:15:24.725>clear.

270
00:15:27.525 --> 00:15:31.945
<00:15:27.525>And <00:15:27.699>then <00:15:27.875>we <00:15:28.050>have <00:15:28.225>other <00:15:28.400>require <00:15:28.574>requires <00:15:28.750>annotations <00:15:28.925>like,

271
00:15:33.845 --> 00:15:38.245
<00:15:33.845>um, <00:15:34.000>what <00:15:34.156>the <00:15:34.311>value <00:15:34.467>of <00:15:34.622>the <00:15:34.778>index <00:15:34.933>has <00:15:35.089>to <00:15:35.245>be.

272
00:15:38.505 --> 00:15:43.125
<00:15:38.505>And <00:15:38.645>later <00:15:38.785>we <00:15:38.925>check <00:15:39.064>if <00:15:39.205>the <00:15:39.345>value <00:15:39.485>is <00:15:39.625>con <00:15:39.765>is <00:15:39.905>in

273
00:15:43.675 --> 00:15:46.205
<00:15:43.675>this <00:15:43.954>insurers <00:15:44.234>is <00:15:44.515>the <00:15:44.795>post <00:15:45.074>conditions,

274
00:15:46.545 --> 00:15:47.725
<00:15:46.545>the <00:15:46.899>insurers <00:15:47.253>are <00:15:47.607>annotations.

275
00:15:48.145 --> 00:15:52.165
<00:15:48.145>If <00:15:48.272>the <00:15:48.399>value <00:15:48.526>is <00:15:48.654>in, <00:15:48.781>then <00:15:48.908>we <00:15:49.035>get <00:15:49.163>the <00:15:49.290>index <00:15:49.417>value <00:15:49.545>returned.

276
00:15:52.225 --> 00:15:54.005
<00:15:52.225>If <00:15:52.458>not, <00:15:52.691>then <00:15:52.925>we <00:15:53.158>get <00:15:53.391>minus <00:15:53.625>one.

277
00:15:56.165 --> 00:15:57.535
<00:15:56.165>What <00:15:56.473>I <00:15:56.781>didn't <00:15:57.089>mention <00:15:57.397>before,

278
00:15:57.535 --> 00:16:00.375
<00:15:57.535>these <00:15:57.662>are <00:15:57.789>the <00:15:57.916>inv <00:15:58.044>variance <00:15:58.171>we <00:15:58.298>have <00:15:58.425>to <00:15:58.553>introduce <00:15:58.680>if <00:15:58.807>we <00:15:58.935>have

279
00:16:00.375 --> 00:16:02.575
<00:16:00.375>to, <00:16:00.575>if <00:16:00.775>we <00:16:00.975>want <00:16:01.175>to <00:16:01.375>check <00:16:01.575>uh, <00:16:01.775>loops.

280
00:16:05.375 --> 00:16:09.315
<00:16:05.375>And <00:16:05.515>here <00:16:05.655>the <00:16:05.795>invariants <00:16:05.935>are <00:16:06.075>introduced <00:16:06.215>also <00:16:06.355>here <00:16:06.495>we <00:16:06.635>can <00:16:06.775>see

281
00:16:09.625 --> 00:16:14.595
<00:16:09.625>what <00:16:09.765>has <00:16:09.905>to <00:16:10.045>be <00:16:10.185>valid <00:16:10.325>during <00:16:10.465>the <00:16:10.605>code <00:16:10.745>is <00:16:10.885>uh, <00:16:11.025>executed.

282
00:16:17.625 --> 00:16:21.355
<00:16:17.625>Then <00:16:17.752>I <00:16:17.879>really <00:16:18.006>had <00:16:18.134>to <00:16:18.261>think <00:16:18.388>that <00:16:18.515>I <00:16:18.643>would <00:16:18.770>not <00:16:18.897>be <00:16:19.025>able

283
00:16:21.355 --> 00:16:24.595
<00:16:21.355>to <00:16:21.495>actually <00:16:21.635>write <00:16:21.775>this <00:16:21.915>code <00:16:22.055>on <00:16:22.195>my <00:16:22.335>own <00:16:22.475>without <00:16:22.615>having <00:16:22.755>a

284
00:16:24.595 --> 00:16:26.515
<00:16:24.595>deeper <00:16:24.945>knowledge <00:16:25.295>in <00:16:25.645>software <00:16:25.995>validation.

285
00:16:28.025 --> 00:16:31.615
<00:16:28.025>Since <00:16:28.199>it <00:16:28.375>you <00:16:28.550>have <00:16:28.725>to <00:16:28.900>be <00:16:29.074>good <00:16:29.250>informal <00:16:29.425>methods

286
00:16:31.675 --> 00:16:32.735
<00:16:31.675>and <00:16:31.992>also <00:16:32.311>in <00:16:32.629>mathematics.

287
00:16:33.955 --> 00:16:37.595
<00:16:33.955>But <00:16:34.188>if <00:16:34.421>we <00:16:34.655>try <00:16:34.888>to <00:16:35.121>use <00:16:35.355>ai,

288
00:16:41.015 --> 00:16:42.755
<00:16:41.015>uh, <00:16:41.365>then <00:16:41.715>things <00:16:42.064>might <00:16:42.415>change.

289
00:16:46.505 --> 00:16:48.475
<00:16:46.505>Just <00:16:46.705>a <00:16:46.905>question. <00:16:47.105>Why <00:16:47.305>to <00:16:47.505>not <00:16:47.705>use <00:16:47.905>ai?

290
00:16:48.485 --> 00:16:52.275
<00:16:48.485>Maybe <00:16:48.660>because <00:16:48.835>it's <00:16:49.010>error <00:16:49.185>prone <00:16:49.360>might <00:16:49.535>produce <00:16:49.710>false <00:16:49.885>positives

291
00:16:52.815 --> 00:16:55.955
<00:16:52.815>and <00:16:53.095>it's <00:16:53.375>not <00:16:53.655>really <00:16:53.935>strict <00:16:54.215>enough.

292
00:16:56.095 --> 00:16:59.755
<00:16:56.095>But <00:16:56.235>again, <00:16:56.375>if <00:16:56.515>you <00:16:56.655>let <00:16:56.795>you <00:16:56.935>code <00:16:57.075>generate <00:16:57.215>by <00:16:57.355>the <00:16:57.495>ai,

293
00:16:59.765 --> 00:17:03.915
<00:16:59.765>maybe <00:16:59.905>you <00:17:00.045>can <00:17:00.185>also <00:17:00.324>use, <00:17:00.465>uh, <00:17:00.605>the <00:17:00.745>proof <00:17:00.885>by <00:17:01.025>the <00:17:01.165>ai.

294
00:17:04.095 --> 00:17:08.605
<00:17:04.095>So <00:17:04.235>it's <00:17:04.375>not <00:17:04.515>nothing <00:17:04.655>against <00:17:04.795>it <00:17:04.935>if <00:17:05.075>you <00:17:05.214>are <00:17:05.355>already <00:17:05.495>ready

295
00:17:08.665 --> 00:17:10.445
<00:17:08.665>to <00:17:08.898>let <00:17:09.131>the <00:17:09.365>AI <00:17:09.598>code <00:17:09.831>for <00:17:10.065>you.

296
00:17:11.715 --> 00:17:15.475
<00:17:11.714>I <00:17:11.855>did <00:17:11.994>the <00:17:12.135>same <00:17:12.274>example <00:17:12.415>like <00:17:12.554>uh, <00:17:12.694>for <00:17:12.834>this <00:17:12.974>binary <00:17:13.115>research

297
00:17:15.505 --> 00:17:18.155
<00:17:15.505>with <00:17:16.205>uh, <00:17:16.905>Gemini

298
00:17:18.735 --> 00:17:20.875
<00:17:18.734>and <00:17:18.890>I <00:17:19.046>was <00:17:19.201>really <00:17:19.357>curious <00:17:19.512>if <00:17:19.668>this <00:17:19.823>works <00:17:19.979>or <00:17:20.135>not.

299
00:17:22.005 --> 00:17:24.815
<00:17:22.005>Then <00:17:22.205>I <00:17:22.405>got <00:17:22.605>this <00:17:22.805>uh, <00:17:23.005>as <00:17:23.205>a <00:17:23.405>result

300
00:17:25.795 --> 00:17:27.085
<00:17:25.795>without <00:17:26.375>changing <00:17:26.956>anything.

301
00:17:28.665 --> 00:17:32.085
<00:17:28.665>And <00:17:28.865>if <00:17:29.065>we <00:17:29.264>really <00:17:29.465>careful <00:17:29.665>look <00:17:29.865>into <00:17:30.065>it,

302
00:17:32.715 --> 00:17:36.725
<00:17:32.715>then <00:17:32.870>we <00:17:33.026>see <00:17:33.181>uh, <00:17:33.337>really <00:17:33.492>something <00:17:33.648>which <00:17:33.803>will <00:17:33.959>not <00:17:34.115>work.

303
00:17:38.355 --> 00:17:41.475
<00:17:38.355>And <00:17:38.635>this <00:17:38.915>is <00:17:39.195>actually <00:17:39.475>the <00:17:39.755>second

304
00:17:41.795 --> 00:17:43.435
<00:17:41.795>requires <00:17:43.195>annotation.

305
00:17:43.495 --> 00:17:48.115
<00:17:43.495>It <00:17:43.622>says <00:17:43.749>the <00:17:43.876>sorted <00:17:44.004>array <00:17:44.131>length <00:17:44.258>is <00:17:44.385>also <00:17:44.513>allowed <00:17:44.640>to <00:17:44.767>be <00:17:44.895>zero.

306
00:17:49.895 --> 00:17:54.315
<00:17:49.895>And <00:17:50.070>in <00:17:50.245>this <00:17:50.420>sense <00:17:50.595>the <00:17:50.770>method <00:17:50.945>will <00:17:51.120>not <00:17:51.295>work.

307
00:17:54.335 --> 00:17:57.075
<00:17:54.335>We <00:17:54.510>get <00:17:54.685>into <00:17:54.860>array <00:17:55.035>index <00:17:55.210>out <00:17:55.385>of <00:17:55.560>bound <00:17:55.735>actually

308
00:17:57.075 --> 00:17:59.435
<00:17:57.075>because <00:17:57.308>there <00:17:57.541>has <00:17:57.775>to <00:17:58.008>be <00:17:58.241>at <00:17:58.475>least

309
00:18:01.875 --> 00:18:04.495
<00:18:01.875>one <00:18:02.030>value <00:18:02.186>in <00:18:02.341>the <00:18:02.497>array <00:18:02.652>so <00:18:02.808>that <00:18:02.963>this <00:18:03.119>stuff <00:18:03.275>works.

310
00:18:05.275 --> 00:18:09.535
<00:18:05.275>And <00:18:05.402>here <00:18:05.529>I <00:18:05.656>had <00:18:05.784>to <00:18:05.911>say, <00:18:06.038>okay, <00:18:06.165>AI <00:18:06.293>might <00:18:06.420>work <00:18:06.547>for <00:18:06.675>it,

311
00:18:09.595 --> 00:18:12.015
<00:18:09.595>but <00:18:09.770>then <00:18:09.945>if <00:18:10.120>you <00:18:10.295>really <00:18:10.470>know <00:18:10.645>what <00:18:10.820>you're <00:18:10.995>doing,

312
00:18:12.025 --> 00:18:16.055
<00:18:12.025>maybe <00:18:12.165>you <00:18:12.305>can <00:18:12.445>fix <00:18:12.585>it <00:18:12.725>and <00:18:12.865>it'll <00:18:13.005>cost <00:18:13.145>you <00:18:13.285>less <00:18:13.425>time.

313
00:18:16.835 --> 00:18:19.295
<00:18:16.835>And <00:18:17.035>all <00:18:17.235>the <00:18:17.435>other <00:18:17.635>stuff <00:18:17.835>is <00:18:18.035>really <00:18:18.235>correct.

314
00:18:19.435 --> 00:18:24.165
<00:18:19.435>And <00:18:19.575>I <00:18:19.715>was <00:18:19.855>really <00:18:19.995>surprised <00:18:20.135>that <00:18:20.274>you <00:18:20.415>can <00:18:20.554>use <00:18:20.695>it <00:18:20.835>for

315
00:18:25.035 --> 00:18:26.605
<00:18:25.035>verifying <00:18:25.735>validating <00:18:26.435>code.

316
00:18:27.345 --> 00:18:30.905
<00:18:27.345>And <00:18:27.520>it <00:18:27.695>is <00:18:27.870>something <00:18:28.045>I <00:18:28.220>will <00:18:28.395>do <00:18:28.570>maybe, <00:18:28.745>uh,

317
00:18:30.905 --> 00:18:35.105
<00:18:30.905>in <00:18:31.080>my <00:18:31.254>future <00:18:31.430>work <00:18:31.605>just <00:18:31.780>to <00:18:31.955>try <00:18:32.129>extracting, <00:18:32.305>uh,

318
00:18:35.255 --> 00:18:39.435
<00:18:35.255>code <00:18:35.488>snippets <00:18:35.721>from, <00:18:35.955>uh, <00:18:36.188>from <00:18:36.421>the <00:18:36.655>project

319
00:18:39.735 --> 00:18:42.475
<00:18:39.735>and <00:18:40.014>adding <00:18:40.294>some <00:18:40.574>validation <00:18:40.854>in <00:18:41.135>just

320
00:18:42.495 --> 00:18:43.915
<00:18:42.495>to <00:18:42.707>check <00:18:42.920>if <00:18:43.134>this <00:18:43.347>works <00:18:43.560>or <00:18:43.773>not.

321
00:18:45.115 --> 00:18:47.855
<00:18:45.115>And <00:18:45.315>hopefully <00:18:45.515>it <00:18:45.715>comes <00:18:45.915>to <00:18:46.115>a <00:18:46.315>point <00:18:46.515>that's

322
00:18:48.165 --> 00:18:51.895
<00:18:48.165>that <00:18:48.292>we <00:18:48.419>can <00:18:48.546>then <00:18:48.674>say, <00:18:48.801>yeah, <00:18:48.928>we <00:18:49.055>don't <00:18:49.183>have <00:18:49.310>to <00:18:49.437>write <00:18:49.565>this

323
00:18:52.445 --> 00:18:55.295
<00:18:52.445>test <00:18:52.620>any <00:18:52.794>longer <00:18:52.970>so <00:18:53.145>we <00:18:53.320>can <00:18:53.495>validate <00:18:53.669>our <00:18:53.845>code

324
00:18:55.515 --> 00:18:58.575
<00:18:55.515>and <00:18:55.690>we <00:18:55.865>can <00:18:56.040>validate <00:18:56.215>the <00:18:56.390>code <00:18:56.565>which <00:18:56.740>is <00:18:56.915>generated.

325
00:18:59.075 --> 00:19:01.095
<00:18:59.075>So <00:18:59.355>software <00:18:59.635>developers <00:18:59.915>maybe <00:19:00.195>don't <00:19:00.475>have

326
00:19:01.115 --> 00:19:02.775
<00:19:01.115>to <00:19:01.465>think <00:19:01.815>about <00:19:02.165>their <00:19:02.515>jobs,

327
00:19:03.955 --> 00:19:06.815
<00:19:03.955>but <00:19:04.095>they <00:19:04.235>can <00:19:04.375>do, <00:19:04.514>when <00:19:04.655>everything <00:19:04.794>is <00:19:04.935>done <00:19:05.074>by <00:19:05.215>the <00:19:05.355>ai,

328
00:19:07.485 --> 00:19:09.935
<00:19:07.485>they <00:19:07.718>can <00:19:07.951>maybe <00:19:08.185>switch <00:19:08.418>to <00:19:08.651>validating <00:19:08.885>code.

329
00:19:12.375 --> 00:19:14.015
<00:19:12.375>Actually, <00:19:12.655>this <00:19:12.935>was <00:19:13.215>already <00:19:13.495>my <00:19:13.775>talk.

330
00:19:14.475 --> 00:19:17.245
<00:19:14.475>It <00:19:14.754>was <00:19:15.034>about, <00:19:15.314>uh, <00:19:15.594>these <00:19:15.875>topics.

331
00:19:17.605 --> 00:19:19.845
<00:19:17.605>I <00:19:17.805>hope <00:19:18.005>you <00:19:18.205>get <00:19:18.405>an <00:19:18.605>insight <00:19:18.805>into <00:19:19.005>it

332
00:19:19.865 --> 00:19:21.285
<00:19:19.865>and <00:19:20.120>you <00:19:20.376>can <00:19:20.631>take <00:19:20.887>something <00:19:21.143>away

333
00:19:21.425 --> 00:19:23.805
<00:19:21.425>and <00:19:21.625>maybe <00:19:21.825>think <00:19:22.024>about <00:19:22.225>it <00:19:22.425>if <00:19:22.625>it <00:19:22.825>fits

334
00:19:23.805 --> 00:19:24.885
<00:19:23.805>somewhere <00:19:24.129>in <00:19:24.453>your <00:19:24.777>business.

335
00:19:25.665 --> 00:19:28.685
<00:19:25.665>And <00:19:25.820>if <00:19:25.976>you <00:19:26.131>have <00:19:26.287>any <00:19:26.442>questions, <00:19:26.598>I <00:19:26.753>will <00:19:26.909>be <00:19:27.065>around.

336
00:19:28.945 --> 00:19:31.125
<00:19:28.945>You <00:19:29.072>can <00:19:29.199>come <00:19:29.326>to <00:19:29.454>me <00:19:29.581>and <00:19:29.708>you <00:19:29.835>can <00:19:29.963>talk <00:19:30.090>about <00:19:30.217>this <00:19:30.345>topic.

337
00:19:33.015 --> 00:19:33.765
<00:19:33.015>Thank <00:19:33.240>you <00:19:33.465>very <00:19:33.690>much.