Parallel Block: Blanking

Simple verification example case where multiple sorts of data structures are "blanked" (that is, `0` is assigned to each element); first a single variable, then an array, and finally a matrix. All three sorts are connected via consecutive parallel blocks.

General information

ID118
Articlenone
Back-endSilicon
LanguagePVL
FeaturesArrays, Iteration contracts, Matrices, Quantified permissions, Statically-scoped parallelism
Sources
Path to example fileparallel/zero-many.pvl
Date2017-06-20

Statistical information

Lines of code36 lines (comments not included)
Lines of specification17 lines (47.22% of the total)
Computation time53406 milliseconds

Example code

Note, verification may take a while and has a time-out of 20 seconds.