Proof of a program: Find. A proof is given of the correctness of the algorithm “Find.” First, an informal description is given of the purpose of the program and the method used. A systematic technique is described for constructing the program proof during the process of coding it, in such a way as to prevent the intrusion of logical errors. The proof of termination is treated as a separate exercise. Finally, some conclusions relating to general programming methodology are drawn.

References in zbMATH (referenced in 81 articles )

Showing results 1 to 20 of 81.
Sorted by year (citations)

1 2 3 4 5 next

  1. Edelkamp, Stefan; Weiß, Armin; Wild, Sebastian: QuickXsort: a fast sorting scheme in theory and practice (2020)
  2. Apt, Krzysztof R.; Olderog, Ernst-Rüdiger: Fifty years of Hoare’s logic (2019)
  3. Dumitrescu, Adrian: A selectable sloppy heap (2019)
  4. Ge, Cunjing; Ma, Feifei; Zhang, Peng; Zhang, Jian: Computing and estimating the volume of the solution space of SMT(LA) constraints (2018)
  5. Goldstein, Larry: Non-asymptotic distributional bounds for the Dickman approximation of the running time of the Quickselect algorithm (2018)
  6. Cloud, Kirkwood; Huber, Mark: Fast perfect simulation of Vervaat perpetuities (2017)
  7. Hook, James: Max-plus algebraic statistical leverage scores (2017)
  8. Jones, Cliff B.: Turing’s 1949 paper in context (2017)
  9. Külekci, M. Oğuzhan; Thankachan, Sharma V.: Range selection and predecessor queries in data aware space and time (2017)
  10. Ngo, Phuc; Kenmochi, Yukiko; Sugimoto, Akihiro; Talbot, Hugues; Passat, Nicolas: Discrete rigid registration: a local graph-search approach (2017)
  11. Barbay, Jérémy; Gupta, Ankur; Satti, Srinivasa Rao; Sorenson, Jon: Near-optimal online multiselection in internal and external memory (2016)
  12. Feltman, Nicolas; Angiuli, Carlo; Acar, Umut A.; Fatahalian, Kayvon: Automatically splitting a two-stage lambda calculus (2016)
  13. Nebel, Markus E.; Wild, Sebastian; Martínez, Conrado: Analysis of pivot sampling in dual-pivot Quicksort: a holistic analysis of Yaroslavskiy’s partitioning scheme (2016)
  14. Wild, Sebastian; Nebel, Markus E.; Mahmoud, Hosam: Analysis of quickselect under Yaroslavskiy’s dual-pivoting algorithm (2016)
  15. Crochemore, Maxime; Grossi, Roberto; Kärkkäinen, Juha; Landau, Gad M.: Computing the Burrows-Wheeler transform in place and in small space (2015)
  16. Amossen, Rasmus Resen; Campagna, Andrea; Pagh, Rasmus: Better size estimation for sparse matrix products (2014)
  17. Duch, Amalia; Jiménez, Rosa M.; Martínez, Conrado: Selection by rank in K-dimensional binary search trees (2014)
  18. Ragab, Mahmoud; Roesler, Uwe: The quicksort process (2014)
  19. Smirnov, Pavel O.; Shevlyakov, Georgy L.: Fast highly efficient and robust one-step (M)-estimators of scale based on (Q_n) (2014)
  20. Fill, James Allen: Distributional convergence for the number of symbol comparisons used by QuickSort (2013)

1 2 3 4 5 next