DSpace Kolekcja:
http://hdl.handle.net/11320/8115
Fri, 09 Aug 2024 20:48:46 GMT2024-08-09T20:48:46ZPartial Correctness of a Power Algorithm
http://hdl.handle.net/11320/8136
Tytuł: Partial Correctness of a Power Algorithm
Autorzy: Jaszczak, Adrian
Abstrakt: This work continues a formal verification of algorithms written in terms of simple-named complex-valued nominative data [6],[8],[15],[11],[12],[13]. In this paper we present a formalization in the Mizar system [3],[1] of the partial correctness of the algorithm: i := val.1 j := val.2 b := val.3 n := val.4 s := val.5 while (i <> n) i := i + j s := s * b return s computing the natural n power of given complex number b, where variables i, b, n, s are located as values of a V-valued Function, loc, as: loc/.1 = i, loc/.3 = b, loc/.4 = n and loc/.5 = s, and the constant 1 is located in the location loc/.2 = j (set V represents simple names of considered nominative data [17]).The validity of the algorithm is presented in terms of semantic Floyd-Hoare triples over such data [9]. Proofs of the correctness are based on an inference system for an extended Floyd-Hoare logic [2],[4] with partial pre- and post-conditions [14],[16],[7],[5].Tue, 01 Jan 2019 00:00:00 GMThttp://hdl.handle.net/11320/81362019-01-01T00:00:00ZPartial Correctness of a Factorial Algorithm
http://hdl.handle.net/11320/8135
Tytuł: Partial Correctness of a Factorial Algorithm
Autorzy: Jaszczak, Adrian; KorniĆowicz, Artur
Abstrakt: In this paper we present a formalization in the Mizar system [3],[1] of the partial correctness of the algorithm: i := val.1 j := val.2 n := val.3 s := val.4 while (i <> n) i := i + j s := s * i return s computing the factorial of given natural number n, where variables i, n, s are located as values of a V-valued Function, loc, as: loc/.1 = i, loc/.3 = n and loc/.4 = s, and the constant 1 is located in the location loc/.2 = j (set V represents simple names of considered nominative data [16]).This work continues a formal verification of algorithms written in terms of simple-named complex-valued nominative data [6],[8],[14],[10],[11],[12]. The validity of the algorithm is presented in terms of semantic Floyd-Hoare triples over such data [9]. Proofs of the correctness are based on an inference system for an extended Floyd-Hoare logic [2],[4] with partial pre- and post-conditions [13],[15],[7],[5].Tue, 01 Jan 2019 00:00:00 GMThttp://hdl.handle.net/11320/81352019-01-01T00:00:00ZAbout Supergraphs. Part III
http://hdl.handle.net/11320/8134
Tytuł: About Supergraphs. Part III
Autorzy: Koch, Sebastian
Abstrakt: The previous articles [5] and [6] introduced formalizations of the step-by-step operations we use to construct finite graphs by hand. That implicitly showed that any finite graph can be constructed from the trivial edgeless graph K1 by applying a finite sequence of these basic operations. In this article that claim is proven explicitly with Mizar[4].Tue, 01 Jan 2019 00:00:00 GMThttp://hdl.handle.net/11320/81342019-01-01T00:00:00ZNatural Addition of Ordinals
http://hdl.handle.net/11320/8133
Tytuł: Natural Addition of Ordinals
Autorzy: Koch, Sebastian
Abstrakt: In [3] the existence of the Cantor normal form of ordinals was proven in the Mizar system [6]. In this article its uniqueness is proven and then used to formalize the natural sum of ordinals.Tue, 01 Jan 2019 00:00:00 GMThttp://hdl.handle.net/11320/81332019-01-01T00:00:00Z