Verification of Procedural Programs via Building their Generalized Nets Models

Магдалина Василева Тодорова - В статията е описан подход за верификация на процедурни програми чрез изграждане на техни модели, дефинирани чрез обобщени мрежи. Подходът интегрира концепцията “design by contract” с подходи за верификация от тип доказателство на теореми и проверка на съгласуваност на модели. За целта разделно се верифицират функциите, които изграждат програмата относно спецификации според предназначението им. Изгражда се обобщен мрежов модел, специфициащ връзките между функциите във вид на коректни редици от извиквания. За главната функция на програмата се построява обобщен мрежов модел и се проверява дали той съответства на мрежовия модел на връзките между функциите на програмата. Всяка от функциите на програмата, която използва други функции се верифицира и относно спецификацията, зададена чрез мрежовия модел на връзките между функциите на програмата.

The Wiener, Eccentric Connectivity and Zagreb Indices of the Hierarchical Product of Graphs

Let G1 = (V1, E1) and G2 = (V2, E2) be two graphs having a distinguished or root vertex, labeled 0. The hierarchical product G2 ⊓ G1 of G2 and G1 is a graph with vertex set V2 × V1. Two vertices y2y1 and x2x1 are adjacent if and only if y1x1 ∈ E1 and y2 = x2; or y2x2 ∈ E2 and y1 = x1 = 0. In this paper, the Wiener, eccentric connectivity and Zagreb indices of this new operation of graphs are computed. As an application, these topological indices for a class of alkanes are computed. ACM Computing Classification System (1998): G.2.2, G.2.3.