| Attributes | Values |
|---|
| rdf:type
| |
| Description
| - In the last decades we got used to software applications (or computers, if you like) being everywhere and working for us. Yet sometimes they fail to work as desired. The current situation is often characterized as the second software crisis. There are many alleged causes of this state. They include, inter alia, web net overload, loss of data, inconsistency of data, intrusions by hackers, etc. etc. Yet in our opinion, the main problem is an old one. It consists in an insufficient specification of the procedures to be executed. We have been dealing with this problem since the beginning of computer era. Though there are many specification methods and languages, the problem remains very much a live issue and so far no satisfactory solution has been found. Our stance is that a declarative logical specification is needed. A serious candidate for such a high-quality declarative specification is a higher-order logic equipped with a procedural semantics. The goal of our contribution is to describe a specification method using Transparent Intensional Logic (TIL). TIL is a hyperintensional, typed, partial lambda-calculus. Hyperintensional, because the meaning of TIL-terms are not the functions/mappings themselves; rather, they are procedures producing functions as their products. Proper typing makes it possible to define inputs and outputs of a procedure. Finally, we must take into account partiality and the possibility of a failure to produce a product. A procedure may fail to produce a correct product for one of two reasons. Either the mapping the procedure produces is undefined at the argument(s) serving as point(s) of evaluation, or the procedure is ill- or under-specified, in which case the empirical execution process has undesirable results. This paper investigates, in a logically rigorous manner, how a detailed specification can prevent these problems.
- In the last decades we got used to software applications (or computers, if you like) being everywhere and working for us. Yet sometimes they fail to work as desired. The current situation is often characterized as the second software crisis. There are many alleged causes of this state. They include, inter alia, web net overload, loss of data, inconsistency of data, intrusions by hackers, etc. etc. Yet in our opinion, the main problem is an old one. It consists in an insufficient specification of the procedures to be executed. We have been dealing with this problem since the beginning of computer era. Though there are many specification methods and languages, the problem remains very much a live issue and so far no satisfactory solution has been found. Our stance is that a declarative logical specification is needed. A serious candidate for such a high-quality declarative specification is a higher-order logic equipped with a procedural semantics. The goal of our contribution is to describe a specification method using Transparent Intensional Logic (TIL). TIL is a hyperintensional, typed, partial lambda-calculus. Hyperintensional, because the meaning of TIL-terms are not the functions/mappings themselves; rather, they are procedures producing functions as their products. Proper typing makes it possible to define inputs and outputs of a procedure. Finally, we must take into account partiality and the possibility of a failure to produce a product. A procedure may fail to produce a correct product for one of two reasons. Either the mapping the procedure produces is undefined at the argument(s) serving as point(s) of evaluation, or the procedure is ill- or under-specified, in which case the empirical execution process has undesirable results. This paper investigates, in a logically rigorous manner, how a detailed specification can prevent these problems. (en)
|
| Title
| - Logical specification of processes
- Logical specification of processes (en)
|
| skos:prefLabel
| - Logical specification of processes
- Logical specification of processes (en)
|
| skos:notation
| - RIV/61989100:27240/14:86086808!RIV15-MSM-27240___
|
| http://linked.open...avai/riv/aktivita
| |
| http://linked.open...avai/riv/aktivity
| |
| http://linked.open...iv/cisloPeriodika
| |
| http://linked.open...vai/riv/dodaniDat
| |
| http://linked.open...aciTvurceVysledku
| |
| http://linked.open.../riv/druhVysledku
| |
| http://linked.open...iv/duvernostUdaju
| |
| http://linked.open...titaPredkladatele
| |
| http://linked.open...dnocenehoVysledku
| |
| http://linked.open...ai/riv/idVysledku
| - RIV/61989100:27240/14:86086808
|
| http://linked.open...riv/jazykVysledku
| |
| http://linked.open.../riv/klicovaSlova
| - TIL; partiality; types; procedural semantics; program specification (en)
|
| http://linked.open.../riv/klicoveSlovo
| |
| http://linked.open...odStatuVydavatele
| |
| http://linked.open...ontrolniKodProRIV
| |
| http://linked.open...i/riv/nazevZdroje
| - Frontiers in Artificial Intelligence and Applications
|
| http://linked.open...in/vavai/riv/obor
| |
| http://linked.open...ichTvurcuVysledku
| |
| http://linked.open...cetTvurcuVysledku
| |
| http://linked.open...vavai/riv/projekt
| |
| http://linked.open...UplatneniVysledku
| |
| http://linked.open...v/svazekPeriodika
| |
| http://linked.open...iv/tvurceVysledku
| - Duží, Marie
- Menšík, Marek
- Číhalová, Martina
|
| issn
| |
| number of pages
| |
| http://bibframe.org/vocab/doi
| - 10.3233/978-1-61499-361-2-45
|
| http://localhost/t...ganizacniJednotka
| |
![[RDF Data]](/fct/images/sw-rdf-blue.png)
![[cxml]](/fct/images/cxml_doc.png)
![[csv]](/fct/images/csv_doc.png)
![[text]](/fct/images/ntriples_doc.png)
![[turtle]](/fct/images/n3turtle_doc.png)
![[ld+json]](/fct/images/jsonld_doc.png)
![[rdf+json]](/fct/images/json_doc.png)
![[rdf+xml]](/fct/images/xml_doc.png)
![[atom+xml]](/fct/images/atom_doc.png)
![[html]](/fct/images/html_doc.png)