search

kframework / k-legacy

The K tools (deprecated, see README)
http://kframework.org
Other
146 stars 61 forks source link

ARRAY module in UIUC K #2349

Closed dwightguth closed 6 years ago

ehildenb commented 6 years ago

Please add tests.

ehildenb commented 6 years ago

What should the semantics of makeArray(5, 0)[7] be? That is, should it return the default value 0, or some error term because 7 it outside the bounds of the array?

dwightguth commented 6 years ago

makeArray(5, 0)[7] and makeArray(5, 0)[7 <- 1][7] should both be zero. The idea behind ARRAY is that an efficient implementation backs an array as an actual array with a fixed length, so any element not explicitly assigned or outside the length of the array is always equal to the default value.

bmmoore commented 6 years ago

As @dwightguth pointed out I missed that we only support one test definition per directory, so making a subdirectory for the tests previously directly in test/builtins is a good idea before making test/builtins/array.