Coding Concepts Overview
This content covers a variety of coding concepts including image objects, git pull, method declaration and definition, algorithm implementation, handling Dafny output errors, and recursion. The discussions range from utilizing schema.org for structuring data to implementing recursive functions such as finding the maximum index in a sequence. Additionally, it explores maintaining invariants during iterative processes and exporting functions with specified conditions.
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author. Download presentation by click this link. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
E N D
Presentation Transcript
git pull! array->seq better comments 2
methods: returns declaration & definition function Donut() : (filling:Filling) ensures Yummy(filling) method Donut() returns filling:Filling { filling := banana; if fruity { return jelly; } filling := creme; } 3
in a method, nobody can hear you scream var isn't let method FindMax(intSeq:seq<int>) returns (maxIndex:nat) requires |intSeq| > 0 ensures maxIndex<|intSeq| ensures forall idx:nat | idx<|intSeq| :: intSeq[idx] <= intSeq[maxIndex] { var count:nat := 0; maxIndex := 0; while(count < |intSeq|) invariant true invariant true invariant true { if(intSeq[maxIndex] < intSeq[count]) { maxIndex := count; } count := count+1; 4
while invariants: requires in, ensures out while(count < |intSeq|) invariant count <= |intSeq| invariant maxIndex < |intSeq| invariant forall prioridx:nat | prioridx<count :: intSeq[prioridx] <= intSeq[maxIndex] { if(intSeq[maxIndex] < intSeq[count]) { maxIndex := count; } count := count+1; } 5
How to ignore Dafny output /home/jonh/summer-school-2021-instructor/chapter06-refine/solutions/exercise01_solution.dfy(353,23): Error: assertion violation Execution trace: (0,0): anon0 (0,0): anon25_Then /home/jonh/summer-school-2021-instructor/chapter06-refine/solutions/exercise01_solution.dfy(358,11): Error: assertion violation Execution trace: (0,0): anon0 /home/jonh/summer-school-2021-instructor/chapter06-refine/solutions/exercise01_solution.dfy(353,5): anon25_Else (0,0): anon26_Then /home/jonh/summer-school-2021-instructor/chapter06-refine/solutions/exercise01_solution.dfy(465,42): Error: possible violation of postcondition of forall statement Execution trace: (0,0): anon0 (0,0): anon26_Else /home/jonh/summer-school-2021-instructor/chapter06-refine/solutions/exercise01_solution.dfy(461,5): anon31_Else (0,0): anon32_Then (0,0): anon33_Then (0,0): anon21 Dafny program verifier finished with 34 verified, 3 errors 6
Recursion: exporting ensures chapter01/demo17.dfy function Evens(count:int) : (outseq:seq<int>) ensures forall idx :: 0<=idx<|outseq| ==> outseq[idx] == 2 * idx { if count==0 then [] else Evens(count) + [2 * (count-1)] } 7
Recursion: use sparingly and replace with forall function Contents(tree: Tree) { { x | exists path :: Resolve(tree, path, x) } } 8
Remainder of Chapter 1 Assignment Exercises 18, 22 and 23 9
