summary refs log tree commit diff stats
path: root/lib/impure
Commit message (Expand)AuthorAgeFilesLines
* fix RST parsing when no indent after enum.item (fix #17249) (#17257)Andrey Makarov2021-03-121-1/+1
* use `-r:off` for runnableExamples that should compile but not run (#17203)Timothee Cour2021-03-011-9/+8
* Change stdlib imports to use std prefix in most examples (#17202)Danil Yarantsev2021-02-286-12/+12
* use single backtick (#17133)flywind2021-02-211-6/+6
* use single backtick (#17115)flywind2021-02-202-153/+153
* use single backtick (#17100)flywind2021-02-184-27/+27
* remove all uses of condsyms symbols defined prior to bootstrap nim 0.20.0 (#1...Timothee Cour2021-02-171-3/+0
* add linenoise.readLineStatus to get status (eg: ctrl-D or ctrl-C) (#16977)Timothee Cour2021-02-091-9/+11
* fix some warnings (#16952)flywind2021-02-081-1/+1
* Deprecate TaintedString (#15423)Juan Carlos2021-01-151-11/+11
* fix #16103 (#16109) [backport:1.0]flywind2020-11-241-5/+21
* fixes #16080 (#16091) [backport:1.2]RokkuCode2020-11-231-1/+1
* fixes db_mysql broken quoting; refs https://github.com/nim-lang/Nim/commit/c1...Andreas Rumpf2020-11-181-1/+0
* Handle BLOB column type in SQLite as binary data (#15681)Regis Caillaud2020-11-021-15/+78
* fixes #15560 (#15587)Andreas Rumpf2020-10-151-2/+1
* various documentation fixes [backport] (#15422)Miran2020-09-291-4/+4
* odbc regression from #14357 (#15417)shirleyquirk2020-09-291-1/+1
* .noalias annotation; frontend support (#15419)Andreas Rumpf2020-09-281-1/+1
* Fix #15219 SQL escape in db_mysql is not enough (#15234)Bung2020-09-041-3/+17
* fixes #15221 (#15230)Andreas Rumpf2020-08-271-1/+1
* better strict funcs, WIP (#15199)Andreas Rumpf2020-08-181-2/+4
* db_postgres document how to use it with unix socket (#15187)Juan Carlos2020-08-171-2/+22
* fix sqlgetdata regression in odbc (#15161)cooldome2020-08-071-12/+8
* An optimizer for ARC (#14962)Andreas Rumpf2020-07-151-5/+5
* Fix style inconsistencies due to the previous commitnarimiran2020-07-061-1/+1
* revert 0944b0f4narimiran2020-07-061-1/+1
* Add jsre (#14870)Juan Carlos2020-07-032-2/+2
* Remove deprecated stuff from stdlib (#14699)Miran2020-06-171-7/+0
* close #14284 document semantics for start for re,nre; improve examples (#14483)Timothee Cour2020-05-282-196/+67
* add bindParams to db_sqlite (#14408)Bung2020-05-261-41/+159
* add insert,tryInsert unify for postgres that need pk name (#14416)Bung2020-05-224-0/+67
* add SqlPrepared api fix #13559 (#14365)Bung2020-05-161-0/+101
* fix #9771 (#14357)Bung2020-05-151-5/+5
* Fail quickly if re or nre module is attempted to be compiled with js [backpor...Kaushal Modi2020-05-142-1/+6
* Error -> Defect for defects (#13908)Jacek Sieka2020-04-281-4/+4
* change some Exceptions to CatchableError or Defect, fixes #10288 (#14069)hlaaftana2020-04-221-1/+1
* fix #7241 (#13779)itsumura-h2020-04-031-0/+5
* Deprecate DCE:on (#13839)Juan Carlos2020-04-022-3/+0
* Add Documentation (#13811)Juan Carlos2020-03-311-2/+8
* Remove 2 old deprecated files (#13702)Juan Carlos2020-03-202-20/+0
* fixes #13654Andreas Rumpf2020-03-161-1/+1
* fix #13218: avoid some irrelevant warnings for nim doc,rst2html,--app:lib, + ...Timothee Cour2020-03-131-1/+1
* make nre compile with --gc:arcAraq2020-01-261-66/+54
* added note to re constructor regarding performance (#13224)whiterock2020-01-221-1/+5
* Check pqntuples > 0 in getValue. Fixes #12973 (#12974)Chris Heller2019-12-291-4/+12
* ported re.nim to ARCAraq2019-12-241-1/+10
* [backport] Fix style issues in lib/, tools/, and testament/. Fixes #12687. (#...3n-k12019-11-281-1/+1
* remove deprecated procs (#12535)Andreas Rumpf2019-11-051-2/+4
* fix several typos in documentation and comments (#12553)Nindaleth2019-10-301-1/+1
* Documentation improvements around the db interface (#12362)Ray Imber2019-10-081-0/+12
generated by cgit-pink 1.4.1-2-gfad0 (git 2.36.2.497.gbbea4dcf42) at 2025-02-07 09:50:33 +0000
pan class="p">:: nim import std / logic proc insertionSort(a: var openArray[int]) {. ensures: forall(i in 1..<a.len, a[i-1] <= a[i]).} = for k in 1 ..< a.len: {.invariant: 1 <= k and k <= a.len.} {.invariant: forall(j in 1..<k, i in 0..<j, a[i] <= a[j]).} var t = k while t > 0 and a[t-1] > a[t]: {.invariant: k < a.len.} {.invariant: 0 <= t and t <= k.} {.invariant: forall(j in 1..k, i in 0..<j, j == t or a[i] <= a[j]).} swap a[t], a[t-1] dec t Unfortunately, the invariants required to prove that this code is correct take more code than the imperative instructions. However, this effort can be compensated by the fact that the result needs very little testing. Be aware though that DrNim only proves that after `insertionSort` this condition holds:: forall(i in 1..<a.len, a[i-1] <= a[i]) This is required, but not sufficient to describe that a `sort` operation was performed. For example, the same postcondition is true for this proc which doesn't sort at all: .. code-block:: nim import std / logic proc insertionSort(a: var openArray[int]) {. ensures: forall(i in 1..<a.len, a[i-1] <= a[i]).} = # does not sort, overwrites `a`'s contents! for i in 0..<a.len: a[i] = i Syntax of propositions ====================== The basic syntax is `ensures|requires|invariant: <prop>`. A `prop` is either a comparison or a compound:: prop = nim_bool_expression | prop 'and' prop | prop 'or' prop | prop '->' prop # implication | prop '<->' prop | 'not' prop | '(' prop ')' # you can group props via () | forallProp | existsProp forallProp = 'forall' '(' quantifierList ',' prop ')' existsProp = 'exists' '(' quantifierList ',' prop ')' quantifierList = quantifier (',' quantifier)* quantifier = <new identifier> 'in' nim_iteration_expression `nim_iteration_expression` here is an ordinary expression of Nim code that describes an iteration space, for example `1..4` or `1..<a.len`. `nim_bool_expression` here is an ordinary expression of Nim code of type `bool` like `a == 3` or `23 > a.len`. The supported subset of Nim code that can be used in these expressions is currently underspecified but `let` variables, function parameters and `result` (which represents the function's final result) are amenable for verification. The expressions must not have any side-effects and must terminate. The operators `forall`, `exists`, `->`, `<->` have to imported from `std / logic`.
generated by cgit-pink 1.4.1-2-gfad0 (git 2.36.2.497.gbbea4dcf42) at 2025-02-07 09:50:30 +0000