東華大學圖書館 |

Weighted Computations : = Semantics and Program Logics = Computacoes Pesadas: Semanticas e Logicas de Programas.

紀錄類型:	書目-電子資源 : Monograph/item
正題名/作者:	Weighted Computations :/
其他題名:	Semantics and Program Logics = Computacoes Pesadas: Semanticas e Logicas de Programas.
其他題名:	Computacoes Pesadas :
作者:	Gomes, Leandro Rafael Moreira.
面頁冊數:	1 online resource (187 pages)
附註:	Source: Dissertations Abstracts International, Volume: 84-07, Section: B.
Contained By:	Dissertations Abstracts International84-07B.
標題:	Medical diagnosis. -
電子資源:	http://pqdd.sinica.edu.tw/twdaoapp/servlet/advanced?query=30227046click for full text (PQDT)
ISBN:	9798368408873

Weighted Computations : = Semantics and Program Logics = Computacoes Pesadas: Semanticas e Logicas de Programas.
Gomes, Leandro Rafael Moreira.

Weighted Computations :Semantics and Program Logics = Computacoes Pesadas: Semanticas e Logicas de Programas.Computacoes Pesadas :Semanticas e Logicas de Programas. - 1 online resource (187 pages)

Source: Dissertations Abstracts International, Volume: 84-07, Section: B.

Thesis (Ph.D.)--Universidade do Minho (Portugal), 2022.

Includes bibliographical references

Esta tese debruca-se sobre computacoes pesadas ou, por outras palavras, programas e assercoes sobre estes cuja execucao ou avaliacao tem alguma forma de peso associado. Por peso queremos dizer um valor que pode representar, por exemplo, uma incerteza na execucao, ou uma quantidade de recursos consumidos, como energia ou tempo. Exemplos de sistemas que contem alguma componente com pesos variam desde comunicacoes entre dispositivos, processos biologicos em rede, sistemas de apoio a decisao clinica ou controlo de robots, estando cada vez mais presentes no nosso quotidiano. Neste sentido, devido a alta complexidade subjacente a introducao destes parametros, exige-se que a engenharia de software recorra a metodologias de desenvolvimento rigorosas para garantir a alta fiabilidade de cada produto de software. E se e verdade que o desenvolvimento, analise e verificacao destes sistemas sao cada vez mais assentes nessa mesma abordagem formal, as praticas correntes de programacao nao sao ainda capazes de oferecer uma estrutura que seja, ao mesmo tempo, generica o suficiente por forma a capturar estes paradigmas e capaz de satisfazer os requisitos especificos para cada dominio de aplicacao.Nos queremos atacar este desafio atraves da apresentacao de uma metodologia de desenvolvimento sistematico de semanticas e logicas para raciocinar sobre duas classes distintas de programas. Na primeira classe, a que nos chamamos de computacao de fluxo unico, cada execucao e uma unica transicao com um peso associado. Na segunda classe, a que nos chamamos computacao de fluxo multiplo, cada execucao pode assumir multiplos caminhos em simultaneo, cada um com um peso possivelmente distinto. Nesta tese definimos, para cada classe de computacao, uma semantica, e provamos que esta forma uma algebra apropriada para raciocinar sobre programas dessa classe. Para esse fim, definimos operadores que interpretam as construcoes basicas de uma linguagem de programacao imperativa: composicao sequencial, condicionais e iteracao. A partir daqui construimos uma logica, incluindo o respetivo sistema axiomatico, que permite verificar propriedades sobre estes programas.Uma das virtudes desta metodologia e a sua parametricidade, que e dada por uma estrutura matematica generica que oferece tanto um modelo de computacao para representar programas como um espaco de verdade para avaliar assercoes sobre eles.Para a classe de computacoes de fluxo unico, definimos tambem uma nocao de bisimilaridade nos modelos dos logicas geradas, provando-se invariancia modal para essas logicas.

Electronic reproduction.
Ann Arbor, Mich. :
ProQuest,
2023

Mode of access: World Wide Web

ISBN: 9798368408873Subjects--Topical Terms:

3684625
Medical diagnosis.
Index Terms--Genre/Form:

542853
Electronic books.

Weighted Computations : = Semantics and Program Logics = Computacoes Pesadas: Semanticas e Logicas de Programas.
LDR:06555nmm a2200457K 4500 001 2353979
005 20230322053954.5
006 m o d
007 cr mn ---uuuuu
008 241011s2022 xx obm 000 0 eng d
020 $a 9798368408873
035 $a (MiAaPQ)AAI30227046
035 $a (MiAaPQ)Portugal182277908
035 $a AAI30227046
040 $a MiAaPQ $b eng $c MiAaPQ $d NTU
100 1 $a Gomes, Leandro Rafael Moreira. $3 3694309
245 1 0 $a Weighted Computations : $b Semantics and Program Logics = Computacoes Pesadas: Semanticas e Logicas de Programas.
246 3 1 $a Computacoes Pesadas : $b Semanticas e Logicas de Programas.
264 0 $c 2022
300 $a 1 online resource (187 pages)
336 $a text $b txt $2 rdacontent
337 $a computer $b c $2 rdamedia
338 $a online resource $b cr $2 rdacarrier
500 $a Source: Dissertations Abstracts International, Volume: 84-07, Section: B.
500 $a Advisor: Barbosa, Luis Soares; Madeira, Alexandre.
502 $a Thesis (Ph.D.)--Universidade do Minho (Portugal), 2022.
504 $a Includes bibliographical references
520 $a Esta tese debruca-se sobre computacoes pesadas ou, por outras palavras, programas e assercoes sobre estes cuja execucao ou avaliacao tem alguma forma de peso associado. Por peso queremos dizer um valor que pode representar, por exemplo, uma incerteza na execucao, ou uma quantidade de recursos consumidos, como energia ou tempo. Exemplos de sistemas que contem alguma componente com pesos variam desde comunicacoes entre dispositivos, processos biologicos em rede, sistemas de apoio a decisao clinica ou controlo de robots, estando cada vez mais presentes no nosso quotidiano. Neste sentido, devido a alta complexidade subjacente a introducao destes parametros, exige-se que a engenharia de software recorra a metodologias de desenvolvimento rigorosas para garantir a alta fiabilidade de cada produto de software. E se e verdade que o desenvolvimento, analise e verificacao destes sistemas sao cada vez mais assentes nessa mesma abordagem formal, as praticas correntes de programacao nao sao ainda capazes de oferecer uma estrutura que seja, ao mesmo tempo, generica o suficiente por forma a capturar estes paradigmas e capaz de satisfazer os requisitos especificos para cada dominio de aplicacao.Nos queremos atacar este desafio atraves da apresentacao de uma metodologia de desenvolvimento sistematico de semanticas e logicas para raciocinar sobre duas classes distintas de programas. Na primeira classe, a que nos chamamos de computacao de fluxo unico, cada execucao e uma unica transicao com um peso associado. Na segunda classe, a que nos chamamos computacao de fluxo multiplo, cada execucao pode assumir multiplos caminhos em simultaneo, cada um com um peso possivelmente distinto. Nesta tese definimos, para cada classe de computacao, uma semantica, e provamos que esta forma uma algebra apropriada para raciocinar sobre programas dessa classe. Para esse fim, definimos operadores que interpretam as construcoes basicas de uma linguagem de programacao imperativa: composicao sequencial, condicionais e iteracao. A partir daqui construimos uma logica, incluindo o respetivo sistema axiomatico, que permite verificar propriedades sobre estes programas.Uma das virtudes desta metodologia e a sua parametricidade, que e dada por uma estrutura matematica generica que oferece tanto um modelo de computacao para representar programas como um espaco de verdade para avaliar assercoes sobre eles.Para a classe de computacoes de fluxo unico, definimos tambem uma nocao de bisimilaridade nos modelos dos logicas geradas, provando-se invariancia modal para essas logicas.
520 $a This thesis deals with weighted computations or, more precisely, programs and assertions about them whose execution or evaluation has some form of weight associated. By weight we mean a value which may represent, for example, an uncertainty in the execution, or a quantity of resources consumed, such as energy or time. Examples of systems containing some component with weights range from device-to-device communications, network biological processes, clinical decision support systems or robot control, being these growingly present in our everyday life. In this sense, due to the complexity underlying the introduction of these parameters, software engineering is forced to call upon rigorous development methodologies which provides a high assurance of each software product. And if it is true that the development, analysis and verification of these systems are increasingly laid on this exactly approach, the current programming practices are not capable to offer a framework which is, at the same time, generic enough to capture such paradigms, and able to satisfy the specific requirements for each application domain.We intend to address this challenge by presenting a methodology for the systematic development of semantics and logics to reason about two distinct classes of programs. In the first class, that we call single-flow computation, each execution is a single transition with an associated weight. In the second class, that we call multi-flow computation, each execution may assume multiple simultaneous execution paths, each one of them with a, possible distinct, weight. In this thesis we define, for each class of computation, a semantics, and we prove that it forms a suitable algebra to reason about programs of that class. For that end, we define operators which interpret the basic constructions of an imperative programming language: sequential composition, conditionals and iteration. From here we construct a logic, including the respective axiomatic system, allowing to verify properties over those programs.One of the merits of this methodology is its parametricity, which is given by a generic mathematical structure offering both a computational model to represent programs and a truth space to evaluate assertions over them.For single-flow computations, we define as well a notion of bisimilarity on the models of the generated logics, and prove the modal invariance property for those logics.
533 $a Electronic reproduction. $b Ann Arbor, Mich. : $c ProQuest, $d 2023
538 $a Mode of access: World Wide Web
650 4 $a Medical diagnosis. $3 3684625
650 4 $a Software. $2 gtt. $3 619355
650 4 $a Programming languages. $3 3683658
650 4 $a Medicine. $3 641104
650 4 $a Syntax. $3 897045
650 4 $a Communication. $3 524709
650 4 $a Boolean. $3 3683493
650 4 $a Logic. $3 529544
650 4 $a Body temperature. $3 916233
650 4 $a Clinical decision making. $3 3694310
650 4 $a Design. $3 518875
650 4 $a Taxonomy. $3 3556303
650 4 $a Energy efficiency. $3 3555643
650 4 $a Algebra. $3 516203
650 4 $a Semantics. $3 520060
650 4 $a Robotics. $3 519753
650 4 $a Computer science. $3 523869
650 4 $a Energy. $3 876794
650 4 $a Linguistics. $3 524476
650 4 $a Mathematics. $3 515831
650 4 $a Physiology. $3 518431
655 7 $a Electronic books. $2 lcsh $3 542853
690 $a 0771
690 $a 0395
690 $a 0389
690 $a 0564
690 $a 0459
690 $a 0984
690 $a 0791
690 $a 0290
690 $a 0405
690 $a 0719
710 2 $a ProQuest Information and Learning Co. $3 783688
710 2 $a Universidade do Minho (Portugal). $3 3437241
773 0 $t Dissertations Abstracts International $g 84-07B.
856 4 0 $u http://pqdd.sinica.edu.tw/twdaoapp/servlet/advanced?query=30227046 $z click for full text (PQDT)